The Born–Fock statement for states

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

Along a gapped C² path Γ with eigenprojector P and physical propagator U_T at speed T (U' = −iT·H U on [0, 1]), a state started in the instantaneous eigenspace stays in it up to O(1/T), uniformly in s ∈ [0, 1]: for ψ₀ ∈ range (P 0),

‖(1 − P s) (U_T s ψ₀)‖ ≤ (C / T) · ‖ψ₀‖.

The two inputs are #161 (U_A s ψ₀ ∈ range (P s) exactly, the adiabatic propagator intertwines the eigenprojections) and #162 (‖U_T s − U_A s‖ ≤ C / T): (1 − P s) U_T ψ₀ = (1 − P s)(U_T − U_A) ψ₀ and ‖1 − P s‖ ≤ 1. Vectors are points of EuclideanSpace ℂ (Fin N) and a matrix acts through Matrix.toEuclideanCLM, so the operator norm of a matrix (L2Operator scope) is exactly the norm of its action.

• Matrix.norm_le_one_of_conjTranspose_mul_self_eq — a Hermitian idempotent has operator norm ≤ 1 (the C*-identity);
• Matrix.norm_toEuclideanCLM_apply_le, norm_toEuclideanCLM_apply_of_conjTranspose_mul_self — ‖A ψ‖ ≤ ‖A‖ ‖ψ‖, and a unitary preserves the norm of a vector;
• Matrix.norm_toEuclideanCLM_apply_sub_le — ‖ψ‖ − ‖(1 − Q) ψ‖ ≤ ‖Q ψ‖;
• GappedPath.norm_proj_le, norm_one_sub_proj_le — ‖P s‖ ≤ 1, ‖1 − P s‖ ≤ 1;
• GappedPath.mem_range_proj_iff — ψ ∈ range (P s) ↔ P s ψ = ψ;
• GappedPath.proj_toEuclideanCLM_apply_of_eq — an eigenvector of H s for lam s is fixed by P s;
• GappedPath.IsPhysPropagator.norm_toEuclideanCLM_apply — ‖U_T s ψ‖ = ‖ψ‖;
• ★ GappedPath.IsAdPropagator.toEuclideanCLM_apply_mem_range, one_sub_proj_toEuclideanCLM_apply — U_A s ψ₀ ∈ range (P s) exactly, i.e. (1 − P s) (U_A s ψ₀) = 0, for ψ₀ ∈ range (P 0);
• ★★ GappedPath.exists_norm_toEuclideanCLM_sub_le — U_T s ψ₀ = U_A s ψ₀ + O(1/T): ‖U_T s ψ − U_A s ψ‖ ≤ (C / T) ‖ψ‖ for every vector ψ;
• ★★★ GappedPath.exists_norm_one_sub_proj_le — the Born–Fock statement: ‖(1 − P s) (U_T s ψ₀)‖ ≤ (C / T) ‖ψ₀‖ for ψ₀ ∈ range (P 0), uniformly on [0, 1];
• ★★ GappedPath.exists_norm_proj_le — the survival form ‖ψ₀‖ − (C / T) ‖ψ₀‖ ≤ ‖P s (U_T s ψ₀)‖.

Honest scope

• The hypotheses are #162's: the path is C², the branch is an eigenvalue at every s, the gap is uniform. C is #162's constant (compactness, not a formula — BACKLOG #166).
• "Probability" statements are the squares of these norm statements for ‖ψ₀‖ = 1 (‖(1 − P s) U_T ψ₀‖² ≤ (C/T)² is the transition probability out of the branch); they are not restated.
• Finite dimensions, L2Operator norm scope, the action of a matrix is Matrix.toEuclideanCLM.

References: M. Born and V. Fock, "Beweis des Adiabatensatzes", Z. Phys. 51 (1928); 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; AdiabaticComparison.lean (#162), AdiabaticPropagators.lean (#161); specs/BACKLOG.md #163, #88.

theorem Matrix.norm_le_one_of_conjTranspose_mul_self_eq {N : ℕ} {Q : Matrix (Fin N) (Fin N) ℂ} (hQ : Q.conjTranspose * Q = Q) : ‖Q‖ ≤ 1

A Hermitian idempotent (Qᴴ Q = Q) has operator norm ≤ 1: the C*-identity gives ‖Q‖² = ‖Qᴴ Q‖ = ‖Q‖.

theorem Matrix.norm_toEuclideanCLM_apply_le {N : ℕ} (A : Matrix (Fin N) (Fin N) ℂ) (x : EuclideanSpace ℂ (Fin N)) : ‖(toEuclideanCLM A) x‖ ≤ ‖A‖ * ‖x‖

‖A ψ‖ ≤ ‖A‖ ‖ψ‖: the L2Operator norm of a matrix bounds its action on Euclidean space.

theorem Matrix.norm_toEuclideanCLM_apply_of_conjTranspose_mul_self {N : ℕ} {U : Matrix (Fin N) (Fin N) ℂ} (hU : U.conjTranspose * U = 1) (x : EuclideanSpace ℂ (Fin N)) : ‖(toEuclideanCLM U) x‖ = ‖x‖

A unitary matrix preserves the norm of a vector.

theorem Matrix.norm_toEuclideanCLM_apply_sub_le {N : ℕ} (Q : Matrix (Fin N) (Fin N) ℂ) (x : EuclideanSpace ℂ (Fin N)) : ‖x‖ - ‖(toEuclideanCLM (1 - Q)) x‖ ≤ ‖(toEuclideanCLM Q) x‖

‖ψ‖ − ‖(1 − Q) ψ‖ ≤ ‖Q ψ‖: the triangle inequality for ψ = Q ψ + (1 − Q) ψ.

theorem Matrix.GappedPath.norm_proj_le {N : ℕ} (Γ : GappedPath N) (s : ℝ) : ‖Γ.proj s‖ ≤ 1

‖P s‖ ≤ 1.

theorem Matrix.GappedPath.norm_one_sub_proj_le {N : ℕ} (Γ : GappedPath N) (s : ℝ) : ‖1 - Γ.proj s‖ ≤ 1

‖1 − P s‖ ≤ 1.

theorem Matrix.GappedPath.mem_range_proj_iff {N : ℕ} (Γ : GappedPath N) (s : ℝ) (x : EuclideanSpace ℂ (Fin N)) : x ∈ Set.range ⇑(toEuclideanCLM (Γ.proj s)) ↔ (toEuclideanCLM (Γ.proj s)) x = x

ψ ∈ range (P s) ↔ P s ψ = ψ (the projector is idempotent).

theorem Matrix.GappedPath.proj_toEuclideanCLM_apply_of_eq {N : ℕ} (Γ : GappedPath N) (s : ℝ) {v : EuclideanSpace ℂ (Fin N)} (hv : (toEuclideanCLM (Γ.H s)) v = ↑(Γ.lam s) • v) : (toEuclideanCLM (Γ.proj s)) v = v

An eigenvector of H s for the branch eigenvalue lies in range (P s): H s v = lam s • v → P s v = v (through X (λ − H) = 1 − P, the reduced resolvent of #162).

theorem Matrix.GappedPath.IsPhysPropagator.norm_toEuclideanCLM_apply {N : ℕ} {Γ : GappedPath N} {T : ℝ} {U : ℝ → Matrix (Fin N) (Fin N) ℂ} (hU : Γ.IsPhysPropagator T U) {s : ℝ} (hs : s ∈ Set.Icc 0 1) (x : EuclideanSpace ℂ (Fin N)) : ‖(toEuclideanCLM (U s)) x‖ = ‖x‖

The physical propagator preserves the norm of a state: ‖U_T s ψ‖ = ‖ψ‖ on [0, 1].

theorem Matrix.GappedPath.IsAdPropagator.proj_toEuclideanCLM_apply {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) {x : EuclideanSpace ℂ (Fin N)} (hx : (toEuclideanCLM (Γ.proj 0)) x = x) : (toEuclideanCLM (Γ.proj s)) ((toEuclideanCLM (U s)) x) = (toEuclideanCLM (U s)) x

★ The adiabatic propagator keeps a state in the instantaneous eigenspace exactly: P s (U_A s ψ₀) = U_A s ψ₀ for P 0 ψ₀ = ψ₀, on [0, 1].

theorem Matrix.GappedPath.IsAdPropagator.toEuclideanCLM_apply_mem_range {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) {x : EuclideanSpace ℂ (Fin N)} (hx : x ∈ Set.range ⇑(toEuclideanCLM (Γ.proj 0))) : (toEuclideanCLM (U s)) x ∈ Set.range ⇑(toEuclideanCLM (Γ.proj s))

U_A s ψ₀ ∈ range (P s) for ψ₀ ∈ range (P 0).

theorem Matrix.GappedPath.IsAdPropagator.one_sub_proj_toEuclideanCLM_apply {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) {x : EuclideanSpace ℂ (Fin N)} (hx : (toEuclideanCLM (Γ.proj 0)) x = x) : (toEuclideanCLM (1 - Γ.proj s)) ((toEuclideanCLM (U s)) x) = 0

(1 − P s) (U_A s ψ₀) = 0 for P 0 ψ₀ = ψ₀.

The Born–Fock statement

theorem Matrix.GappedPath.exists_norm_toEuclideanCLM_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, ∀ (x : EuclideanSpace ℂ (Fin N)), ‖(toEuclideanCLM (UT s)) x - (toEuclideanCLM (UA s)) x‖ ≤ C / T * ‖x‖

★★ U_T s ψ = U_A s ψ + O(1/T): Kato's comparison on vectors, ‖U_T s ψ − U_A s ψ‖ ≤ (C / T) ‖ψ‖ for every ψ, uniformly on [0, 1].

theorem Matrix.GappedPath.exists_norm_one_sub_proj_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 : ℝ → Matrix (Fin N) (Fin N) ℂ), Γ.IsPhysPropagator T UT → ∀ s ∈ Set.Icc 0 1, ∀ (x : EuclideanSpace ℂ (Fin N)), (toEuclideanCLM (Γ.proj 0)) x = x → ‖(toEuclideanCLM (1 - Γ.proj s)) ((toEuclideanCLM (UT s)) x)‖ ≤ C / T * ‖x‖

★★★ The Born–Fock statement. Along a gapped C² path whose branch is an eigenvalue, there is a constant C such that for every speed T > 0, every physical propagator U_T, every s ∈ [0, 1] and every state ψ₀ in the initial eigenspace (P 0 ψ₀ = ψ₀),

‖(1 − P s) (U_T s ψ₀)‖ ≤ (C / T) ‖ψ₀‖:

the solution started in the instantaneous eigenspace stays in it up to O(1/T), uniformly. (C is #162's constant.)

theorem Matrix.GappedPath.exists_norm_proj_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 : ℝ → Matrix (Fin N) (Fin N) ℂ), Γ.IsPhysPropagator T UT → ∀ s ∈ Set.Icc 0 1, ∀ (x : EuclideanSpace ℂ (Fin N)), (toEuclideanCLM (Γ.proj 0)) x = x → ‖x‖ - C / T * ‖x‖ ≤ ‖(toEuclideanCLM (Γ.proj s)) ((toEuclideanCLM (UT s)) x)‖

★★ The survival form: ‖ψ₀‖ − (C / T) ‖ψ₀‖ ≤ ‖P s (U_T s ψ₀)‖ for P 0 ψ₀ = ψ₀ — the component that stays in the branch has norm at least (1 − C/T) ‖ψ₀‖.