The adiabatic intertwiner and Kato's intertwining identity

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #160 (out of #88, the third brick of Kato's adiabatic theorem).

Along a gapped path Γ (RieszProjectorSmooth.lean) with eigenprojector P s, Kato's adiabatic generator is the commutator K s = [Ṗ s, P s] = Ṗ P − P Ṗ, and the adiabatic intertwiner A is the propagator of K (UnitaryPropagator.lean): A' = K A, A 0 = 1. This file shows K is anti-Hermitian and derives, from the general propagator theory, that A exists, is unitary, and carries the initial eigenspace exactly onto the instantaneous one.

• GappedPath.K, continuous_K, ★ conjTranspose_K — the generator is continuous and anti-Hermitian, because the derivative of a Hermitian family is Hermitian (conjTranspose_deriv_proj);
• deriv_proj_sub_comm_K, hasDerivWithinAt_proj_comm — Ṗ = [K, P]: by deriv_proj_eq and proj_mul_deriv_mul_proj (#159), Ṗ − [K, P] = Ṗ − (ṖP + PṖ) + 2 PṖP = 0;
• GappedPath.IsIntertwiner Γ T A — A is a propagator of K on [0, T];
• ★ exists_isIntertwiner — the intertwiner exists;
• ★ IsIntertwiner.conjTranspose_mul_self, mul_conjTranspose, mem_unitaryGroup — A is unitary;
• ★★ IsIntertwiner.mul_proj_zero — Kato's intertwining identity A(s) P(0) = P(s) A(s), the Heisenberg intertwining for Q = P; IsIntertwiner.conjTranspose_mul_proj_mul is the form A† P A ≡ P(0);
• IsIntertwiner.proj_mulVec — a vector in the initial eigenspace is carried into the instantaneous one, exactly;
• IsIntertwiner.unique — any two intertwiners agree on [0, T].

Honest scope

• A is defined on [0, T] by one-sided derivatives at the ends, as the corpus linear-ODE lemma delivers it; T > 0 is arbitrary.
• The path is C¹ (1 ≤ n); nothing is rescaled yet — the propagators at speed T are #161.
• Everything is finite-dimensional and under the L2Operator norm scope.

References: T. Kato, "On the adiabatic theorem of quantum mechanics", J. Phys. Soc. Japan 5 (1950), §2 (the operator A(s) and A P(0) = P A); Kato, Perturbation Theory for Linear Operators, II §4.2; S. Teufel, Adiabatic Perturbation Theory in Quantum Dynamics, §2.1; RieszProjectorSmooth.lean (#159), UnitaryPropagator.lean; specs/BACKLOG.md #160, #88.

The adiabatic generator

noncomputable def Matrix.GappedPath.K {N : ℕ} (Γ : GappedPath N) (s : ℝ) : Matrix (Fin N) (Fin N) ℂ

Kato's adiabatic generator K s = [Ṗ s, P s].

Equations

• Γ.K s = deriv Γ.proj s * Γ.proj s - Γ.proj s * deriv Γ.proj s

theorem Matrix.GappedPath.continuous_K {N : ℕ} (Γ : GappedPath N) {n : ℕ∞} (hn : 1 ≤ n) (hH : ContDiff ℝ (↑n) Γ.H) : Continuous Γ.K

theorem Matrix.GappedPath.conjTranspose_deriv_proj {N : ℕ} (Γ : GappedPath N) {n : ℕ∞} (hn : 1 ≤ n) (hH : ContDiff ℝ (↑n) Γ.H) (s : ℝ) : (deriv Γ.proj s).conjTranspose = deriv Γ.proj s

The derivative of the (Hermitian) eigenprojector is Hermitian.

theorem Matrix.GappedPath.conjTranspose_K {N : ℕ} (Γ : GappedPath N) {n : ℕ∞} (hn : 1 ≤ n) (hH : ContDiff ℝ (↑n) Γ.H) (s : ℝ) : (Γ.K s).conjTranspose = -Γ.K s

★ The adiabatic generator is anti-Hermitian.

theorem Matrix.GappedPath.deriv_proj_sub_comm_K {N : ℕ} (Γ : GappedPath N) {n : ℕ∞} (hn : 1 ≤ n) (hH : ContDiff ℝ (↑n) Γ.H) (s : ℝ) : -(Γ.K s * Γ.proj s) + deriv Γ.proj s + Γ.proj s * Γ.K s = 0

Ṗ − [K, P] = 0: the identity behind the intertwining.

theorem Matrix.GappedPath.hasDerivWithinAt_proj_comm {N : ℕ} (Γ : GappedPath N) {n : ℕ∞} (hn : 1 ≤ n) (hH : ContDiff ℝ (↑n) Γ.H) (T s : ℝ) : s ∈ Set.Icc 0 T → HasDerivWithinAt Γ.proj (Γ.K s * Γ.proj s - Γ.proj s * Γ.K s) (Set.Icc 0 T) s

Ṗ = [K, P], as a derivative statement on [0, T].

The intertwiner

@[reducible, inline]

abbrev Matrix.GappedPath.IsIntertwiner {N : ℕ} (Γ : GappedPath N) (T : ℝ) (A : ℝ → Matrix (Fin N) (Fin N) ℂ) : Prop

A is an adiabatic intertwiner of Γ on [0, T]: a propagator of K, i.e. A 0 = 1 and A' = K A there.

Equations

• Γ.IsIntertwiner T A = Matrix.IsPropagator Γ.K T A

theorem Matrix.GappedPath.exists_isIntertwiner {N : ℕ} (Γ : GappedPath N) {n : ℕ∞} (hn : 1 ≤ n) (hH : ContDiff ℝ (↑n) Γ.H) {T : ℝ} (hT : 0 < T) : ∃ (A : ℝ → Matrix (Fin N) (Fin N) ℂ), Γ.IsIntertwiner T A

★ The adiabatic intertwiner exists on every [0, T].

theorem Matrix.GappedPath.IsIntertwiner.conjTranspose_mul_self {N : ℕ} {Γ : GappedPath N} {T : ℝ} {A : ℝ → Matrix (Fin N) (Fin N) ℂ} (hA : Γ.IsIntertwiner T A) {n : ℕ∞} (hn : 1 ≤ n) (hH : ContDiff ℝ (↑n) Γ.H) (s : ℝ) : s ∈ Set.Icc 0 T → (A s).conjTranspose * A s = 1

★ The intertwiner is unitary: A† A = 1 on [0, T].

theorem Matrix.GappedPath.IsIntertwiner.mul_conjTranspose {N : ℕ} {Γ : GappedPath N} {T : ℝ} {A : ℝ → Matrix (Fin N) (Fin N) ℂ} (hA : Γ.IsIntertwiner T A) {n : ℕ∞} (hn : 1 ≤ n) (hH : ContDiff ℝ (↑n) Γ.H) (s : ℝ) : s ∈ Set.Icc 0 T → A s * (A s).conjTranspose = 1

A A† = 1 on [0, T].

theorem Matrix.GappedPath.IsIntertwiner.mem_unitaryGroup {N : ℕ} {Γ : GappedPath N} {T : ℝ} {A : ℝ → Matrix (Fin N) (Fin N) ℂ} (hA : Γ.IsIntertwiner T A) {n : ℕ∞} (hn : 1 ≤ n) (hH : ContDiff ℝ (↑n) Γ.H) (s : ℝ) : s ∈ Set.Icc 0 T → A s ∈ unitaryGroup (Fin N) ℂ

theorem Matrix.GappedPath.IsIntertwiner.mul_proj_zero {N : ℕ} {Γ : GappedPath N} {T : ℝ} {A : ℝ → Matrix (Fin N) (Fin N) ℂ} (hA : Γ.IsIntertwiner T A) {n : ℕ∞} (hn : 1 ≤ n) (hH : ContDiff ℝ (↑n) Γ.H) (s : ℝ) : s ∈ Set.Icc 0 T → A s * Γ.proj 0 = Γ.proj s * A s

★★ Kato's intertwining identity: A(s) P(0) = P(s) A(s) on [0, T]. The intertwiner carries the initial eigenspace exactly onto the instantaneous one.

theorem Matrix.GappedPath.IsIntertwiner.conjTranspose_mul_proj_mul {N : ℕ} {Γ : GappedPath N} {T : ℝ} {A : ℝ → Matrix (Fin N) (Fin N) ℂ} (hA : Γ.IsIntertwiner T A) {n : ℕ∞} (hn : 1 ≤ n) (hH : ContDiff ℝ (↑n) Γ.H) (s : ℝ) : s ∈ Set.Icc 0 T → (A s).conjTranspose * Γ.proj s * A s = Γ.proj 0

★★ A† P A is constant: A(s)† P(s) A(s) = P(0) on [0, T].

theorem Matrix.GappedPath.IsIntertwiner.proj_mulVec {N : ℕ} {Γ : GappedPath N} {T : ℝ} {A : ℝ → Matrix (Fin N) (Fin N) ℂ} (hA : Γ.IsIntertwiner T A) {n : ℕ∞} (hn : 1 ≤ n) (hH : ContDiff ℝ (↑n) Γ.H) {s : ℝ} (hs : s ∈ Set.Icc 0 T) {v : Fin N → ℂ} (hv : (Γ.proj 0).mulVec v = v) : (Γ.proj s).mulVec ((A s).mulVec v) = (A s).mulVec v

A vector in the initial eigenspace is carried into the instantaneous eigenspace.

theorem Matrix.GappedPath.IsIntertwiner.unique {N : ℕ} {Γ : GappedPath N} {T : ℝ} {A B : ℝ → Matrix (Fin N) (Fin N) ℂ} (hA : Γ.IsIntertwiner T A) (hB : Γ.IsIntertwiner T B) {n : ℕ∞} (hn : 1 ≤ n) (hH : ContDiff ℝ (↑n) Γ.H) (s : ℝ) : s ∈ Set.Icc 0 T → A s = B s

Any two intertwiners agree on [0, T].