Kato's comparison: ‖U_T − U_A‖ ≤ C / T

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

Along a gapped C² path Γ with eigenprojector P, adiabatic generator K = [Ṗ, P], physical propagator U_T (U' = −iT·H U) and adiabatic propagator U_A (U' = (−iT·H + K) U) on [0, 1], the two propagators differ by O(1/T) uniformly:

∃ C, ∀ T > 0, ∀ s ∈ [0, 1], ‖U_T(s) − U_A(s)‖ ≤ C / T.

The proof is Kato's. W = U_T† U_A has W' = U_T† K U_A, and the oscillation of the integrand is what produces the 1/T: write K = Y H − H Y for a C¹ family Y (the reduced resolvent X = (λ − H)⁻¹ (1 − P), and Y = X Ṗ P + P Ṗ X); then (U_T† Y U_A)' = −iT · U_T† K U_A + U_T† (Ẏ + Y K) U_A, so W + (iT)⁻¹ U_T† Y U_A has derivative (iT)⁻¹ U_T† (Ẏ + Y K) U_A, of size O(1/T); the boundary terms are O(1/T) because Y is bounded and the propagators are unitary.

• circleIntegral_sub_inv_mul_self, circleIntegral_sub_inv_mul_sub_inv, circleIntegral_sub_inv_mul_sub_inv_eq — the Cauchy evaluations of ∮ (z−λ)⁻¹ (z−μ)⁻¹ dz (0 for a double pole, 2πi (λ − μ)⁻¹ for μ outside);
• Matrix.redResIntegral, ★ IsHermitian.redResIntegral_eq_conjD — the reduced resolvent as a contour integral (2πi)⁻¹ ∮ (z − λ)⁻¹ (z − H)⁻¹ dz is U diag(0 on the branch, (λ−μⱼ)⁻¹ off it) U†;
• GappedPath.redRes, redRes_eq_conjD, redRes_eq_near, ★★ contDiff_redRes — the reduced resolvent along the path is as smooth as the path (the contour freezes locally, exactly as for P in #159; contDiffOn_circleIntegral);
• smul_one_sub_H_mul_redRes, redRes_mul_smul_one_sub_H, redRes_mul_proj, proj_mul_redRes — (λ − H) X = X (λ − H) = 1 − P, X P = P X = 0;
• GappedPath.Y, contDiff_Y, ★★ Y_mul_H_sub — Y H − H Y = K, pure algebra from the four identities above;
• norm_one_le_one, norm_le_one_of_conjTranspose_mul_self, norm_conjTranspose_mul_mul_le — unitaries have operator norm ≤ 1 (the C*-identity), so ‖U† X V‖ ≤ ‖X‖;
• norm_sub_le_of_hasDerivWithinAt_Icc — the mean-value bound on [0, T];
• ★★ GappedPath.norm_sub_le_of_bounds — the estimate with the two suprema as hypotheses;
• ★★★ GappedPath.exists_norm_sub_le — Kato's comparison.

Honest scope

• C depends on the path only (through sup ‖Y‖ and sup ‖Ẏ + Y K‖ on [0, 1], which exist by compactness here); AdiabaticConstant.lean (#166) makes it the formula 8 M₁/g² + 4 M₂/g² + 80 M₁²/g³ with M₁ ≥ sup ‖Ḣ‖, M₂ ≥ sup ‖Ḧ‖, through norm_sub_le_of_bounds.
• The path is C² (2 ≤ n) and the branch is an eigenvalue at every s (so λ is C² too, #159's contDiff_lam); the gap is uniform.
• Finite dimensions, L2Operator norm scope, one-sided derivatives at the ends.

References: T. Kato, "On the adiabatic theorem of quantum mechanics", J. Phys. Soc. Japan 5 (1950), §3; S. Teufel, Adiabatic Perturbation Theory in Quantum Dynamics, Thm 2.2 and its proof; AdiabaticPropagators.lean (#161), AdiabaticIntertwiner.lean (#160), RieszProjectorSmooth.lean (#159), RieszProjector.lean (#158); specs/BACKLOG.md #162, #88.

Cauchy evaluations of (z − λ)⁻¹ (z − μ)⁻¹

theorem circleIntegral_sub_inv_mul_self (c w : ℂ) (r : ℝ) : ∮ (z : ℂ) in C(c, r), (z - w)⁻¹ * (z - w)⁻¹ = 0

A double pole integrates to zero.

theorem circleIntegral_sub_inv_mul_sub_inv {c lamc μ : ℂ} {r : ℝ} (hlam : dist lamc c < r) (hμ : r < dist μ c) : ∮ (z : ℂ) in C(c, r), (z - lamc)⁻¹ * (z - μ)⁻¹ = 2 * ↑Real.pi * Complex.I * (lamc - μ)⁻¹

For λ inside and μ outside the circle, ∮ (z − λ)⁻¹ (z − μ)⁻¹ dz = 2πi (λ − μ)⁻¹.

theorem circleIntegral_sub_inv_mul_sub_inv_eq {c lamc μ : ℂ} {r : ℝ} (hlam : dist lamc c < r) (hμ : μ = lamc ∨ r < dist μ c) : ∮ (z : ℂ) in C(c, r), (z - lamc)⁻¹ * (z - μ)⁻¹ = if μ = lamc then 0 else 2 * ↑Real.pi * Complex.I * (lamc - μ)⁻¹

The two cases together, for μ either on the branch or outside.

theorem dist_ofReal_ofReal (a b : ℝ) : dist ↑a ↑b = |a - b|

The distance of two reals, in ℂ.

The reduced resolvent as a contour integral

noncomputable def Matrix.redResIntegral {N : ℕ} (H : Matrix (Fin N) (Fin N) ℂ) (c lamc : ℂ) (r : ℝ) : Matrix (Fin N) (Fin N) ℂ

The reduced resolvent integral (2πi)⁻¹ ∮_{C(c, r)} (z − λ)⁻¹ (z·1 − H)⁻¹ dz.

Equations

• H.redResIntegral c lamc r = (2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - lamc)⁻¹ • (z • 1 - H)⁻¹

theorem Matrix.IsHermitian.redResIntegral_eq_conjD {N : ℕ} {H : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) {c lamc : ℂ} {r : ℝ} (hlam : dist lamc c < r) (hout : ∀ (j : Fin N), hH.eigC j = lamc ∨ r < dist (hH.eigC j) c) : H.redResIntegral c lamc r = hH.conjD fun (j : Fin N) => if hH.eigC j = lamc then 0 else (lamc - hH.eigC j)⁻¹

★ The reduced resolvent integral in the eigenbasis: with λ inside the circle and every eigenvalue either equal to λ or outside, it is U diag(0 on the branch, (λ − μⱼ)⁻¹ off it) U†.

Norms of unitaries

theorem Matrix.norm_one_le_one {N : ℕ} : ‖1‖ ≤ 1

theorem Matrix.norm_le_one_of_conjTranspose_mul_self {N : ℕ} {U : Matrix (Fin N) (Fin N) ℂ} (hU : U.conjTranspose * U = 1) : ‖U‖ ≤ 1

A matrix with Uᴴ U = 1 has operator norm at most 1.

theorem Matrix.norm_conjTranspose_mul_mul_le {N : ℕ} {U V : Matrix (Fin N) (Fin N) ℂ} (hU : ‖U‖ ≤ 1) (hV : ‖V‖ ≤ 1) (X : Matrix (Fin N) (Fin N) ℂ) : ‖U.conjTranspose * X * V‖ ≤ ‖X‖

Sandwiching between matrices of norm ≤ 1 does not increase the norm.

The mean-value bound on [0, T]

theorem norm_sub_le_of_hasDerivWithinAt_Icc {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {f f' : ℝ → F} {T C : ℝ} (hf : ∀ s ∈ Set.Icc 0 T, HasDerivWithinAt f (f' s) (Set.Icc 0 T) s) (hb : ∀ s ∈ Set.Icc 0 T, ‖f' s‖ ≤ C) (s : ℝ) : s ∈ Set.Icc 0 T → ‖f s - f 0‖ ≤ C * s

A function whose (one-sided) derivative within [0, T] is bounded by C moves by at most C · s.

The reduced resolvent along the path

theorem Matrix.GappedPath.eigC_eq_iff {N : ℕ} (Γ : GappedPath N) (s : ℝ) (j : Fin N) (x : ℝ) : ⋯.eigC j = ↑x ↔ ⋯.eigenvalues j = x

theorem Matrix.GappedPath.proj_eq_conjD {N : ℕ} (Γ : GappedPath N) (s : ℝ) : Γ.proj s = ⋯.conjD (⋯.discInd (↑(Γ.lam s)) (Γ.g / 2))

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

The reduced resolvent X s = (λ s − H s)⁻¹ (1 − P s), as the contour integral (2πi)⁻¹ ∮_{C(λ s, g/2)} (z − λ s)⁻¹ (z − H s)⁻¹ dz.

Equations

• Γ.redRes s = (Γ.H s).redResIntegral (↑(Γ.lam s)) (↑(Γ.lam s)) (Γ.g / 2)

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

The diagonal of the reduced resolvent: 0 on the branch, (λ − μⱼ)⁻¹ off it.

Equations

• Γ.rr s j = if ⋯.eigC j = ↑(Γ.lam s) then 0 else (↑(Γ.lam s) - ⋯.eigC j)⁻¹

theorem Matrix.GappedPath.hout_near {N : ℕ} (Γ : GappedPath N) {s s₀ : ℝ} (h : |Γ.lam s - Γ.lam s₀| < Γ.g / 4) (j : Fin N) : ⋯.eigC j = ↑(Γ.lam s) ∨ Γ.g / 2 < dist (⋯.eigC j) ↑(Γ.lam s₀)

Off the branch, every eigenvalue is outside the disc of radius g/2 about a point within g/4 of the branch.

theorem Matrix.GappedPath.redRes_eq_conjD {N : ℕ} (Γ : GappedPath N) (s : ℝ) : Γ.redRes s = ⋯.conjD (Γ.rr s)

theorem Matrix.GappedPath.redRes_eq_near {N : ℕ} (Γ : GappedPath N) {s s₀ : ℝ} (h : |Γ.lam s - Γ.lam s₀| < Γ.g / 4) : Γ.redRes s = (Γ.H s).redResIntegral (↑(Γ.lam s₀)) (↑(Γ.lam s)) (Γ.g / 2)

The contour freezes locally: for |λ s − λ s₀| < g/4, the reduced resolvent at s is the integral over the fixed circle about λ s₀.

theorem Matrix.GappedPath.contDiff_redRes {N : ℕ} (Γ : GappedPath N) {n : ℕ∞} (hH : ContDiff ℝ (↑n) Γ.H) (hex : ∀ (s : ℝ), ∃ (j : Fin N), ⋯.eigenvalues j = Γ.lam s) : ContDiff ℝ (↑n) Γ.redRes

★★ The reduced resolvent is as smooth as the path.

The algebra of the reduced resolvent

theorem Matrix.GappedPath.redRes_mul_proj {N : ℕ} (Γ : GappedPath N) (s : ℝ) : Γ.redRes s * Γ.proj s = 0

theorem Matrix.GappedPath.proj_mul_redRes {N : ℕ} (Γ : GappedPath N) (s : ℝ) : Γ.proj s * Γ.redRes s = 0

theorem Matrix.GappedPath.conjD_lam_sub_mul_rr {N : ℕ} (Γ : GappedPath N) (s : ℝ) : ⋯.conjD ((fun (j : Fin N) => ↑(Γ.lam s) - ⋯.eigC j) * Γ.rr s) = 1 - Γ.proj s

The diagonal identity (λ − μⱼ) · rrⱼ = 1 − 𝟙_branch.

theorem Matrix.GappedPath.smul_one_sub_H_mul_redRes {N : ℕ} (Γ : GappedPath N) (s : ℝ) : (↑(Γ.lam s) • 1 - Γ.H s) * Γ.redRes s = 1 - Γ.proj s

(λ − H) X = 1 − P.

theorem Matrix.GappedPath.redRes_mul_smul_one_sub_H {N : ℕ} (Γ : GappedPath N) (s : ℝ) : Γ.redRes s * (↑(Γ.lam s) • 1 - Γ.H s) = 1 - Γ.proj s

X (λ − H) = 1 − P.

The family Y with Y H − H Y = K

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

Kato's Y = X Ṗ P + P Ṗ X.

Equations

• Γ.Y s = Γ.redRes s * deriv Γ.proj s * Γ.proj s + Γ.proj s * deriv Γ.proj s * Γ.redRes s

theorem Matrix.GappedPath.Y_mul_H_sub {N : ℕ} (Γ : GappedPath N) (s : ℝ) : Γ.Y s * Γ.H s - Γ.H s * Γ.Y s = Γ.K s

★★ Y H − H Y = K: pure algebra from (λ − H) X = X (λ − H) = 1 − P and (λ − H) P = 0.

theorem Matrix.GappedPath.contDiff_Y {N : ℕ} (Γ : GappedPath N) {n : ℕ∞} (hn : 2 ≤ n) (hH : ContDiff ℝ (↑n) Γ.H) (hex : ∀ (s : ℝ), ∃ (j : Fin N), ⋯.eigenvalues j = Γ.lam s) : ContDiff ℝ 1 Γ.Y

Y is C¹ along a gapped C² path.

Kato's comparison

theorem Matrix.GappedPath.norm_sub_le_of_bounds {N : ℕ} (Γ : GappedPath N) {n : ℕ∞} (hn : 2 ≤ n) (hH : ContDiff ℝ (↑n) Γ.H) (hex : ∀ (s : ℝ), ∃ (j : Fin N), ⋯.eigenvalues j = Γ.lam s) {MY ME : ℝ} (hMY : ∀ s ∈ Set.Icc 0 1, ‖Γ.Y s‖ ≤ MY) (hME : ∀ s ∈ Set.Icc 0 1, ‖deriv Γ.Y s + Γ.Y s * Γ.K s‖ ≤ ME) {T : ℝ} (hT : 0 < T) {UT UA : ℝ → Matrix (Fin N) (Fin N) ℂ} (hUT : Γ.IsPhysPropagator T UT) (hUA : Γ.IsAdPropagator T UA) (s : ℝ) : s ∈ Set.Icc 0 1 → ‖UT s - UA s‖ ≤ (2 * MY + ME) / T

★★ The estimate behind Kato's comparison, with the two suprema as explicit hypotheses: if ‖Y‖ ≤ MY and ‖Ẏ + Y K‖ ≤ ME on [0, 1], then ‖U_T(s) − U_A(s)‖ ≤ (2 MY + ME) / T.

theorem Matrix.GappedPath.exists_norm_sub_le {N : ℕ} (Γ : GappedPath N) {n : ℕ∞} (hn : 2 ≤ n) (hH : ContDiff ℝ (↑n) Γ.H) (hex : ∀ (s : ℝ), ∃ (j : Fin N), ⋯.eigenvalues j = Γ.lam s) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (T : ℝ), 0 < T → ∀ (UT UA : ℝ → Matrix (Fin N) (Fin N) ℂ), Γ.IsPhysPropagator T UT → Γ.IsAdPropagator T UA → ∀ s ∈ Set.Icc 0 1, ‖UT s - UA s‖ ≤ C / T

★★★ Kato's comparison. Along a gapped C² path whose branch is an eigenvalue, there is a constant C such that, for every speed T > 0, the physical and the adiabatic propagators satisfy ‖U_T(s) − U_A(s)‖ ≤ C / T for all s ∈ [0, 1]. (AdiabaticConstant.lean makes C explicit.)