Unitary propagators of a time-dependent anti-Hermitian generator

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #160/#161 (out of #88): the common core of the adiabatic intertwiner and of the two propagators of Kato's adiabatic theorem.

For a continuous G : ℝ → Matrix (Fin N) (Fin N) ℂ, a propagator of G on [0, T] is a solution U of U' = G U, U 0 = 1 (one-sided derivatives at the ends). This file proves what the adiabatic theorem uses about such solutions when G is anti-Hermitian, all by one device — the derivative of U† Y vanishes whenever Y' = G Y, so U† Y is constant:

• eq_of_hasDerivWithinAt_zero_Icc — a function with zero derivative within [0, T] is constant;
• conjTransposeCLM, HasDerivWithinAt.matrixConjTranspose — the conjugate transpose is a continuous ℝ-linear map, so it commutes with derivatives;
• IsPropagator G T U — the solution property;
• ★ exists_isPropagator — a propagator exists for every continuous G and every T > 0 (exists_linearODE_solution_Icc with the coefficient ContinuousLinearMap.mul ℝ _ (G s));
• IsPropagator.conjTranspose_mul_eq — the Heisenberg constancy: U† Y ≡ Y 0 for every solution Y' = G Y;
• ★ IsPropagator.conjTranspose_mul_self, mul_conjTranspose, mem_unitaryGroup — the propagator of an anti-Hermitian generator is unitary;
• IsPropagator.eq_mul_init — uniqueness: every solution of Y' = G Y is U · Y 0; IsPropagator.unique — two propagators agree;
• ★ IsPropagator.mul_eq_of_hasDerivWithinAt_comm — the Heisenberg intertwining: if Q' = [G, Q] then U(s) Q(0) = Q(s) U(s).

Honest scope

Finite dimensions, L2Operator norm scope, one-sided derivatives on Icc 0 T. Anti-Hermitian means (G s)ᴴ = −G s on [0, T]; nothing is assumed off the interval.

References: T. Kato, "On the adiabatic theorem of quantum mechanics", J. Phys. Soc. Japan 5 (1950); Analysis/ODE/FlowDerivative.lean (exists_linearODE_solution_Icc); specs/BACKLOG.md #160, #161, #88.

A derivative-free family is constant on [0, T]

theorem eq_of_hasDerivWithinAt_zero_Icc {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : ℝ → F} {T : ℝ} (hf : ∀ s ∈ Set.Icc 0 T, HasDerivWithinAt f 0 (Set.Icc 0 T) s) (s : ℝ) : s ∈ Set.Icc 0 T → f s = f 0

A function with zero (one-sided) derivative within [0, T] at every point of [0, T] is constant there.

The conjugate transpose as a continuous ℝ-linear map

noncomputable def Matrix.conjTransposeCLM {N : ℕ} : Matrix (Fin N) (Fin N) ℂ →L[ℝ] Matrix (Fin N) (Fin N) ℂ

The conjugate transpose, as a continuous ℝ-linear map.

Equations

• Matrix.conjTransposeCLM = LinearMap.toContinuousLinearMap { toFun := fun (A : Matrix (Fin N) (Fin N) ℂ) => A.conjTranspose, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Matrix.conjTransposeCLM_apply {N : ℕ} (A : Matrix (Fin N) (Fin N) ℂ) : conjTransposeCLM A = A.conjTranspose

theorem Matrix.HasDerivWithinAt.matrixConjTranspose {N : ℕ} {A : ℝ → Matrix (Fin N) (Fin N) ℂ} {A' : Matrix (Fin N) (Fin N) ℂ} {s : Set ℝ} {t : ℝ} (h : HasDerivWithinAt A A' s t) : HasDerivWithinAt (fun (u : ℝ) => (A u).conjTranspose) A'.conjTranspose s t

The derivative of the conjugate transpose is the conjugate transpose of the derivative.

theorem Matrix.HasDerivAt.matrixConjTranspose {N : ℕ} {A : ℝ → Matrix (Fin N) (Fin N) ℂ} {A' : Matrix (Fin N) (Fin N) ℂ} {t : ℝ} (h : HasDerivAt A A' t) : HasDerivAt (fun (u : ℝ) => (A u).conjTranspose) A'.conjTranspose t

Propagators

structure Matrix.IsPropagator {N : ℕ} (G : ℝ → Matrix (Fin N) (Fin N) ℂ) (T : ℝ) (U : ℝ → Matrix (Fin N) (Fin N) ℂ) : Prop

U is a propagator of the generator G on [0, T]: U 0 = 1 and U' = G U there.

• init : U 0 = 1
• hasDerivWithinAt (s : ℝ) : s ∈ Set.Icc 0 T → HasDerivWithinAt U (G s * U s) (Set.Icc 0 T) s

theorem Matrix.exists_isPropagator {N : ℕ} {G : ℝ → Matrix (Fin N) (Fin N) ℂ} {T : ℝ} (hT : 0 < T) (hG : ContinuousOn G (Set.Icc 0 T)) : ∃ (U : ℝ → Matrix (Fin N) (Fin N) ℂ), IsPropagator G T U

★ A propagator exists for every generator continuous on [0, T], T > 0.

theorem Matrix.IsPropagator.conjTranspose_mul_eq {N : ℕ} {G : ℝ → Matrix (Fin N) (Fin N) ℂ} {T : ℝ} {U Y : ℝ → Matrix (Fin N) (Fin N) ℂ} (hU : IsPropagator G T U) (hG : ∀ s ∈ Set.Icc 0 T, (G s).conjTranspose = -G s) (hY : ∀ s ∈ Set.Icc 0 T, HasDerivWithinAt Y (G s * Y s) (Set.Icc 0 T) s) (s : ℝ) : s ∈ Set.Icc 0 T → (U s).conjTranspose * Y s = Y 0

The Heisenberg constancy: for an anti-Hermitian generator, U† Y is constant along every solution Y' = G Y.

theorem Matrix.IsPropagator.conjTranspose_mul_self {N : ℕ} {G : ℝ → Matrix (Fin N) (Fin N) ℂ} {T : ℝ} {U : ℝ → Matrix (Fin N) (Fin N) ℂ} (hU : IsPropagator G T U) (hG : ∀ s ∈ Set.Icc 0 T, (G s).conjTranspose = -G s) (s : ℝ) : s ∈ Set.Icc 0 T → (U s).conjTranspose * U s = 1

★ The propagator of an anti-Hermitian generator is unitary: U† U = 1 on [0, T].

theorem Matrix.IsPropagator.mul_conjTranspose {N : ℕ} {G : ℝ → Matrix (Fin N) (Fin N) ℂ} {T : ℝ} {U : ℝ → Matrix (Fin N) (Fin N) ℂ} (hU : IsPropagator G T U) (hG : ∀ s ∈ Set.Icc 0 T, (G s).conjTranspose = -G s) (s : ℝ) : s ∈ Set.Icc 0 T → U s * (U s).conjTranspose = 1

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

theorem Matrix.IsPropagator.mem_unitaryGroup {N : ℕ} {G : ℝ → Matrix (Fin N) (Fin N) ℂ} {T : ℝ} {U : ℝ → Matrix (Fin N) (Fin N) ℂ} (hU : IsPropagator G T U) (hG : ∀ s ∈ Set.Icc 0 T, (G s).conjTranspose = -G s) (s : ℝ) : s ∈ Set.Icc 0 T → U s ∈ unitaryGroup (Fin N) ℂ

theorem Matrix.IsPropagator.eq_mul_init {N : ℕ} {G : ℝ → Matrix (Fin N) (Fin N) ℂ} {T : ℝ} {U Y : ℝ → Matrix (Fin N) (Fin N) ℂ} (hU : IsPropagator G T U) (hG : ∀ s ∈ Set.Icc 0 T, (G s).conjTranspose = -G s) (hY : ∀ s ∈ Set.Icc 0 T, HasDerivWithinAt Y (G s * Y s) (Set.Icc 0 T) s) (s : ℝ) : s ∈ Set.Icc 0 T → Y s = U s * Y 0

Uniqueness: every solution of Y' = G Y on [0, T] is U · Y 0.

theorem Matrix.IsPropagator.unique {N : ℕ} {G : ℝ → Matrix (Fin N) (Fin N) ℂ} {T : ℝ} {U V : ℝ → Matrix (Fin N) (Fin N) ℂ} (hU : IsPropagator G T U) (hV : IsPropagator G T V) (hG : ∀ s ∈ Set.Icc 0 T, (G s).conjTranspose = -G s) (s : ℝ) : s ∈ Set.Icc 0 T → U s = V s

Two propagators of the same anti-Hermitian generator agree on [0, T].

theorem Matrix.IsPropagator.mul_eq_of_hasDerivWithinAt_comm {N : ℕ} {G : ℝ → Matrix (Fin N) (Fin N) ℂ} {T : ℝ} {U : ℝ → Matrix (Fin N) (Fin N) ℂ} (hU : IsPropagator G T U) (hG : ∀ s ∈ Set.Icc 0 T, (G s).conjTranspose = -G s) {Q : ℝ → Matrix (Fin N) (Fin N) ℂ} (hQ : ∀ s ∈ Set.Icc 0 T, HasDerivWithinAt Q (G s * Q s - Q s * G s) (Set.Icc 0 T) s) (s : ℝ) : s ∈ Set.Icc 0 T → U s * Q 0 = Q s * U s

★ The Heisenberg intertwining: if Q' = [G, Q] on [0, T], then U(s) Q(0) = Q(s) U(s) there.