The two propagators at speed T

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

In the rescaled time s = t/T along a gapped path Γ with Hamiltonian H s, eigenprojector P s and adiabatic generator K s = [Ṗ, P]:

• the physical propagator U_T solves U' = −iT·H(s) U, U 0 = 1 — the Schrödinger evolution traversed at speed T;
• the adiabatic propagator U_A solves U' = (−iT·H(s) + K(s)) U, U 0 = 1.

Both are propagators of anti-Hermitian generators (UnitaryPropagator.lean), so both exist on [0, 1] and are unitary. The adiabatic one intertwines the eigenprojections exactly, and on the initial eigenspace it is the intertwiner A of #160 times a dynamical phase.

• GappedPath.physGen, adGen, conjTranspose_physGen, conjTranspose_adGen — the two generators, anti-Hermitian; IsPhysPropagator Γ T U, IsAdPropagator Γ T U;
• ★ exists_isPhysPropagator, ★ exists_isAdPropagator, and the unitarity of both (IsPhysPropagator.conjTranspose_mul_self, …, IsAdPropagator.mem_unitaryGroup);
• ★★ IsAdPropagator.mul_proj_zero — U_A(s) P(0) = P(s) U_A(s): P commutes with H, so [adGen, P] = [K, P] = Ṗ and the Heisenberg intertwining applies;
• GappedPath.dynPhase T s = exp(−iT ∫₀ˢ lam) — the dynamical phase;
• ★★ IsAdPropagator.mul_proj_zero_eq — on the initial eigenspace, U_A is the dynamical phase times the intertwiner: U_A(s) P(0) = e^{−iT∫₀ˢ lam} · A(s) P(0). The rescaled Z = e^{+iT∫lam} U_A P(0) solves Z' = K Z with Z 0 = P(0), because H U_A P(0) = lam · U_A P(0) by the intertwining; uniqueness for the propagator A of K finishes. No multiplicity assumption: the identity holds for a degenerate branch as well.

Honest scope

• T : ℝ is any real (the speed); the physical content is T → ∞, which is #162.
• The interval is [0, 1], one-sided at the ends; the path is C¹ for the adiabatic propagator and merely continuous for the physical one.
• Finite dimensions, L2Operator norm scope.

References: T. Kato, J. Phys. Soc. Japan 5 (1950), §2; S. Teufel, Adiabatic Perturbation Theory in Quantum Dynamics, §2.1 (U^ε_a, the adiabatic evolution); AdiabaticIntertwiner.lean (#160), UnitaryPropagator.lean, QuantumInfo/RotatingFrame.lean (the constant-generator and rigidly rotated propagators that preceded these); specs/BACKLOG.md #161, #88.

The two generators

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

The physical generator at speed T: −iT·H(s).

Equations

• Γ.physGen T s = (-Complex.I * ↑T) • Γ.H s

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

The adiabatic generator at speed T: −iT·H(s) + K(s).

Equations

• Γ.adGen T s = Γ.physGen T s + Γ.K s

theorem Matrix.GappedPath.continuous_physGen {N : ℕ} (Γ : GappedPath N) {n : ℕ∞} (hH : ContDiff ℝ (↑n) Γ.H) (T : ℝ) : Continuous (Γ.physGen T)

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

theorem Matrix.GappedPath.conjTranspose_physGen {N : ℕ} (Γ : GappedPath N) (T s : ℝ) : (Γ.physGen T s).conjTranspose = -Γ.physGen T s

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

theorem Matrix.GappedPath.adGen_mul_proj_sub {N : ℕ} (Γ : GappedPath N) (T s : ℝ) : Γ.adGen T s * Γ.proj s - Γ.proj s * Γ.adGen T s = Γ.K s * Γ.proj s - Γ.proj s * Γ.K s

[adGen, P] = [K, P]: the Hamiltonian commutes with its eigenprojector.

The propagators

@[reducible, inline]

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

U is the physical propagator at speed T on [0, 1]: U 0 = 1, U' = −iT·H U.

Equations

• Γ.IsPhysPropagator T U = Matrix.IsPropagator (Γ.physGen T) 1 U

@[reducible, inline]

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

U is the adiabatic propagator at speed T on [0, 1]: U 0 = 1, U' = (−iT·H + K) U.

Equations

• Γ.IsAdPropagator T U = Matrix.IsPropagator (Γ.adGen T) 1 U

theorem Matrix.GappedPath.exists_isPhysPropagator {N : ℕ} (Γ : GappedPath N) {n : ℕ∞} (hH : ContDiff ℝ (↑n) Γ.H) (T : ℝ) : ∃ (U : ℝ → Matrix (Fin N) (Fin N) ℂ), Γ.IsPhysPropagator T U

★ The physical propagator exists.

theorem Matrix.GappedPath.exists_isAdPropagator {N : ℕ} (Γ : GappedPath N) {n : ℕ∞} (hn : 1 ≤ n) (hH : ContDiff ℝ (↑n) Γ.H) (T : ℝ) : ∃ (U : ℝ → Matrix (Fin N) (Fin N) ℂ), Γ.IsAdPropagator T U

★ The adiabatic propagator exists.

theorem Matrix.GappedPath.IsPhysPropagator.conjTranspose_mul_self {N : ℕ} {Γ : GappedPath N} {T : ℝ} {U : ℝ → Matrix (Fin N) (Fin N) ℂ} (hU : Γ.IsPhysPropagator T U) (s : ℝ) : s ∈ Set.Icc 0 1 → (U s).conjTranspose * U s = 1

The physical propagator is unitary.

theorem Matrix.GappedPath.IsPhysPropagator.mul_conjTranspose {N : ℕ} {Γ : GappedPath N} {T : ℝ} {U : ℝ → Matrix (Fin N) (Fin N) ℂ} (hU : Γ.IsPhysPropagator T U) (s : ℝ) : s ∈ Set.Icc 0 1 → U s * (U s).conjTranspose = 1

theorem Matrix.GappedPath.IsPhysPropagator.mem_unitaryGroup {N : ℕ} {Γ : GappedPath N} {T : ℝ} {U : ℝ → Matrix (Fin N) (Fin N) ℂ} (hU : Γ.IsPhysPropagator T U) (s : ℝ) : s ∈ Set.Icc 0 1 → U s ∈ unitaryGroup (Fin N) ℂ

The dynamical phase

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

The dynamical phase exp(−iT ∫₀ˢ lam).

Equations

• Γ.dynPhase T s = Complex.exp (-Complex.I * ↑T * ↑(∫ (t : ℝ) in 0..s, Γ.lam t))

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

The inverse dynamical phase exp(+iT ∫₀ˢ lam).

Equations

• Γ.invDynPhase T s = Complex.exp (Complex.I * ↑T * ↑(∫ (t : ℝ) in 0..s, Γ.lam t))

theorem Matrix.GappedPath.dynPhase_mul_invDynPhase {N : ℕ} (Γ : GappedPath N) (T s : ℝ) : Γ.dynPhase T s * Γ.invDynPhase T s = 1

theorem Matrix.GappedPath.invDynPhase_zero {N : ℕ} (Γ : GappedPath N) (T : ℝ) : Γ.invDynPhase T 0 = 1

theorem Matrix.GappedPath.hasDerivAt_invDynPhase {N : ℕ} (Γ : GappedPath N) (T s : ℝ) : HasDerivAt (Γ.invDynPhase T) (Γ.invDynPhase T s * (Complex.I * ↑T * ↑(Γ.lam s))) s

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

The adiabatic propagator is unitary.

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

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

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

★★ The adiabatic propagator intertwines the eigenprojections exactly: U_A(s) P(0) = P(s) U_A(s) on [0, 1].

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

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

theorem Matrix.GappedPath.IsAdPropagator.H_mul_mul_proj_zero {N : ℕ} {Γ : GappedPath N} {T : ℝ} {U : ℝ → Matrix (Fin N) (Fin N) ℂ} (hU : Γ.IsAdPropagator T U) {n : ℕ∞} (hn : 1 ≤ n) (hH : ContDiff ℝ (↑n) Γ.H) {s : ℝ} (hs : s ∈ Set.Icc 0 1) : Γ.H s * (U s * Γ.proj 0) = ↑(Γ.lam s) • (U s * Γ.proj 0)

H(s) · U_A(s) P(0) = lam s · U_A(s) P(0): the propagated eigenspace is still the lam s-eigenspace.

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

★★ On the initial eigenspace, the adiabatic propagator is the dynamical phase times the intertwiner: U_A(s) P(0) = e^{−iT∫₀ˢ lam} · A(s) P(0) on [0, 1], for any multiplicity.