An explicit adiabatic constant

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #166 (out of #162): the constant of Kato's comparison as a formula in the gap and the derivatives of the path.

#162 proved ‖U_T(s) − U_A(s)‖ ≤ C / T with C = 2 sup‖Y‖ + sup‖Ẏ + Y K‖ by compactness. Here every quantity is bounded in terms of the gap g, M₁ ≥ sup_{[0,1]} ‖Ḣ‖ and M₂ ≥ sup_{[0,1]} ‖Ḧ‖:

C = 8 M₁ / g² + 4 M₂ / g² + 80 M₁² / g³.

The row expected this to need the derivative of the Riesz projector as a contour integral. It does not: differentiating H P = P H and multiplying by the reduced resolvent X gives Ṗ = X Ḣ P + P Ḣ X (Kato's formula) by pure algebra from X (λ − H) = 1 − P, X P = P X = 0, P Ṗ P = 0; differentiating X (λ − H) = 1 − P and X P = 0 gives Ẋ likewise, with λ̇ P = P Ḣ P for the eigenvalue's derivative. The norms then follow from ‖P‖ ≤ 1 and ‖X‖ ≤ 1/g (the operator norm of U diag(d) U† is sup |dⱼ|).

• Matrix.IsHermitian.norm_conjD_le, GappedPath.norm_rr_le, ★ norm_redRes_le — ‖X‖ ≤ 1/g;
• one_le_norm_of_mul_self_eq, GappedPath.proj_ne_zero, one_le_norm_proj — ‖P‖ ≥ 1;
• GappedPath.hasDerivAt_H, hasDerivAt_lam, hasDerivAt_redRes, hasDerivAt_deriv_H, hasDerivAt_deriv_proj, contDiff_one_deriv_of_two — the derivatives that exist;
• GappedPath.redRes_mul_H, H_mul_redRes, deriv_H_mul_proj_add — X H = λ X − (1 − P) and Ḣ P + H Ṗ = Ṗ H + P Ḣ;
• ★★ GappedPath.deriv_proj_mul_proj, proj_mul_deriv_proj, deriv_proj_eq_redRes — Ṗ P = X Ḣ P, P Ṗ = P Ḣ X, Ṗ = X Ḣ P + P Ḣ X;
• ★ GappedPath.proj_mul_deriv_H_mul_proj — P Ḣ P = λ̇ P, and norm_deriv_lam_le: |λ̇| ≤ ‖Ḣ‖;
• ★★ GappedPath.deriv_redRes_eq — Ẋ = −Ṗ X − λ̇ X² + X Ḣ X − X Ṗ;
• GappedPath.hasDerivAt_deriv_proj_eq, hasDerivAt_Y — P̈ and Ẏ by the product rule;
• GappedPath.norm_deriv_proj_le, norm_deriv_redRes_le, norm_deriv_deriv_proj_le, norm_Y_le, norm_K_le, norm_deriv_Y_add_le — the pointwise bounds ‖Ṗ‖ ≤ 2M₁/g, ‖Ẋ‖ ≤ 6M₁/g², ‖P̈‖ ≤ 16M₁²/g² + 2M₂/g, ‖Y‖ ≤ 4M₁/g², ‖K‖ ≤ 4M₁/g, ‖Ẏ + Y K‖ ≤ 80M₁²/g³ + 4M₂/g²;
• ★★★ GappedPath.norm_sub_le_explicit — Kato's comparison with an explicit constant.

Honest scope

• The constants 8, 4, 80 are what the termwise triangle inequality gives; they are not optimal (Teufel's Thm 2.2 has the same shape with smaller numbers obtained by a sharper route). The spin-½ instance (#165) has an exact overlap error ≤ (2π(π+2)/g) · ω/(2π), well inside this.
• M₁, M₂ bound ‖Ḣ‖, ‖Ḧ‖ on [0, 1] in the L2Operator norm; C² path, uniform gap, the branch an eigenvalue, as in #162.

References: T. Kato, Perturbation Theory for Linear Operators, II-§2.3 (the derivative of the reduced resolvent); S. Teufel, Adiabatic Perturbation Theory in Quantum Dynamics, Thm 2.2; AdiabaticComparison.lean (#162, norm_sub_le_of_bounds); specs/BACKLOG.md #166, #162.

theorem contDiff_one_deriv_of_two {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} (hn : 2 ≤ n) {f : ℝ → F} (hf : ContDiff ℝ (↑n) f) : ContDiff ℝ 1 (deriv f)

A C² function has a C¹ derivative.

theorem norm_mul_mul_le {R : Type u_1} [NonUnitalSeminormedRing R] (A B C : R) : ‖A * (B * C)‖ ≤ ‖A‖ * (‖B‖ * ‖C‖)

theorem norm_mul_mul_le' {R : Type u_1} [NonUnitalSeminormedRing R] (A B C : R) : ‖A * B * C‖ ≤ ‖A‖ * ‖B‖ * ‖C‖

theorem norm_mul_add_mul_le {R : Type u_1} [NonUnitalSeminormedRing R] (A B C D E : R) : ‖A * (B * C + D * E)‖ ≤ ‖A‖ * (‖B‖ * ‖C‖ + ‖D‖ * ‖E‖)

theorem norm_add_mul_mul_le {R : Type u_1} [NonUnitalSeminormedRing R] (A B C D E : R) : ‖(A * B + C * D) * E‖ ≤ (‖A‖ * ‖B‖ + ‖C‖ * ‖D‖) * ‖E‖

theorem Matrix.IsHermitian.norm_conjD_le {N : ℕ} {H : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) (d : Fin N → ℂ) : ‖hH.conjD d‖ ≤ ‖d‖

‖U diag(d) U†‖ ≤ sup |dⱼ|.

theorem Matrix.one_le_norm_of_mul_self_eq {N : ℕ} {P : Matrix (Fin N) (Fin N) ℂ} (hP : P * P = P) (h0 : P ≠ 0) : 1 ≤ ‖P‖

A nonzero idempotent has operator norm ≥ 1.

‖X‖ ≤ 1/g and ‖P‖ ≥ 1

theorem Matrix.GappedPath.norm_rr_le {N : ℕ} (Γ : GappedPath N) (s : ℝ) : ‖Γ.rr s‖ ≤ 1 / Γ.g

theorem Matrix.GappedPath.norm_redRes_le {N : ℕ} (Γ : GappedPath N) (s : ℝ) : ‖Γ.redRes s‖ ≤ 1 / Γ.g

★ ‖X‖ ≤ 1/g: the reduced resolvent is bounded by the inverse gap.

theorem Matrix.GappedPath.proj_ne_zero {N : ℕ} (Γ : GappedPath N) {s : ℝ} (hex : ∃ (j : Fin N), ⋯.eigenvalues j = Γ.lam s) : Γ.proj s ≠ 0

theorem Matrix.GappedPath.one_le_norm_proj {N : ℕ} (Γ : GappedPath N) {s : ℝ} (hex : ∃ (j : Fin N), ⋯.eigenvalues j = Γ.lam s) : 1 ≤ ‖Γ.proj s‖

The derivatives that exist

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

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

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

theorem Matrix.GappedPath.hasDerivAt_deriv_H {N : ℕ} (Γ : GappedPath N) {n : ℕ∞} (hn : 2 ≤ n) (hH : ContDiff ℝ (↑n) Γ.H) (s : ℝ) : HasDerivAt (deriv Γ.H) (deriv (deriv Γ.H) s) s

theorem Matrix.GappedPath.hasDerivAt_deriv_proj {N : ℕ} (Γ : GappedPath N) {n : ℕ∞} (hn : 2 ≤ n) (hH : ContDiff ℝ (↑n) Γ.H) (s : ℝ) : HasDerivAt (deriv Γ.proj) (deriv (deriv Γ.proj) s) s

The algebra: Ṗ = X Ḣ P + P Ḣ X, P Ḣ P = λ̇ P, Ẋ

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

X H = λ X − (1 − P).

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

H X = λ X − (1 − P).

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

Differentiating H P = P H: Ḣ P + H Ṗ = Ṗ H + P Ḣ.

theorem Matrix.GappedPath.proj_mul_H_mul {N : ℕ} (Γ : GappedPath N) (s : ℝ) (M : Matrix (Fin N) (Fin N) ℂ) : Γ.proj s * (Γ.H s * M) = ↑(Γ.lam s) • (Γ.proj s * M)

theorem Matrix.GappedPath.redRes_mul_proj_mul {N : ℕ} (Γ : GappedPath N) (s : ℝ) (M : Matrix (Fin N) (Fin N) ℂ) : Γ.redRes s * (Γ.proj s * M) = 0

theorem Matrix.GappedPath.proj_mul_proj_mul {N : ℕ} (Γ : GappedPath N) (s : ℝ) (M : Matrix (Fin N) (Fin N) ℂ) : Γ.proj s * (Γ.proj s * M) = Γ.proj s * M

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

theorem Matrix.GappedPath.redRes_mul_H_mul {N : ℕ} (Γ : GappedPath N) (s : ℝ) (M : Matrix (Fin N) (Fin N) ℂ) : Γ.redRes s * (Γ.H s * M) = ↑(Γ.lam s) • (Γ.redRes s * M) - M + Γ.proj s * M

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

★★ Ṗ P = X Ḣ P.

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

★★ P Ṗ = P Ḣ X.

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

★★ Kato's formula Ṗ = X Ḣ P + P Ḣ X, by algebra alone.

theorem Matrix.GappedPath.deriv_H_mul_proj_add_eq {N : ℕ} (Γ : GappedPath N) {n : ℕ∞} (hn : 1 ≤ n) (hH : ContDiff ℝ (↑n) Γ.H) (hex : ∀ (s : ℝ), ∃ (j : Fin N), ⋯.eigenvalues j = Γ.lam s) (s : ℝ) : deriv Γ.H s * Γ.proj s + Γ.H s * deriv Γ.proj s = ↑(deriv Γ.lam s) • Γ.proj s + ↑(Γ.lam s) • deriv Γ.proj s

Differentiating H P = λ P: Ḣ P + H Ṗ = λ̇ P + λ Ṗ.

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

★ P Ḣ P = λ̇ P: the eigenvalue's derivative is the branch expectation of Ḣ.

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

|λ̇| ≤ ‖Ḣ‖.

theorem Matrix.GappedPath.deriv_redRes_mul_proj_add {N : ℕ} (Γ : GappedPath N) {n : ℕ∞} (hn : 1 ≤ n) (hH : ContDiff ℝ (↑n) Γ.H) (hex : ∀ (s : ℝ), ∃ (j : Fin N), ⋯.eigenvalues j = Γ.lam s) (s : ℝ) : deriv Γ.redRes s * Γ.proj s + Γ.redRes s * deriv Γ.proj s = 0

Differentiating X P = 0: Ẋ P + X Ṗ = 0.

theorem Matrix.GappedPath.deriv_redRes_mul_add {N : ℕ} (Γ : GappedPath N) {n : ℕ∞} (hn : 1 ≤ n) (hH : ContDiff ℝ (↑n) Γ.H) (hex : ∀ (s : ℝ), ∃ (j : Fin N), ⋯.eigenvalues j = Γ.lam s) (s : ℝ) : deriv Γ.redRes s * (↑(Γ.lam s) • 1 - Γ.H s) + Γ.redRes s * (↑(deriv Γ.lam s) • 1 - deriv Γ.H s) = -deriv Γ.proj s

Differentiating X (λ − H) = 1 − P: Ẋ (λ − H) + X (λ̇ − Ḣ) = −Ṗ.

theorem Matrix.GappedPath.deriv_redRes_eq {N : ℕ} (Γ : GappedPath N) {n : ℕ∞} (hn : 1 ≤ n) (hH : ContDiff ℝ (↑n) Γ.H) (hex : ∀ (s : ℝ), ∃ (j : Fin N), ⋯.eigenvalues j = Γ.lam s) (s : ℝ) : deriv Γ.redRes s = -(deriv Γ.proj s * Γ.redRes s) - ↑(deriv Γ.lam s) • (Γ.redRes s * Γ.redRes s) + Γ.redRes s * (deriv Γ.H s * Γ.redRes s) - Γ.redRes s * deriv Γ.proj s

★★ The derivative of the reduced resolvent: Ẋ = −Ṗ X − λ̇ X² + X Ḣ X − X Ṗ (Kato II-§2.3).

P̈ and Ẏ

theorem Matrix.GappedPath.hasDerivAt_deriv_proj_eq {N : ℕ} (Γ : GappedPath N) {n : ℕ∞} (hn : 2 ≤ n) (hH : ContDiff ℝ (↑n) Γ.H) (hex : ∀ (s : ℝ), ∃ (j : Fin N), ⋯.eigenvalues j = Γ.lam s) (s : ℝ) : deriv (deriv Γ.proj) s = deriv Γ.redRes s * (deriv Γ.H s * Γ.proj s) + Γ.redRes s * (deriv (deriv Γ.H) s * Γ.proj s + deriv Γ.H s * deriv Γ.proj s) + (deriv Γ.proj s * (deriv Γ.H s * Γ.redRes s) + Γ.proj s * (deriv (deriv Γ.H) s * Γ.redRes s + deriv Γ.H s * deriv Γ.redRes s))

P̈ by differentiating Ṗ = X Ḣ P + P Ḣ X.

theorem Matrix.GappedPath.hasDerivAt_Y {N : ℕ} (Γ : GappedPath N) {n : ℕ∞} (hn : 2 ≤ n) (hH : ContDiff ℝ (↑n) Γ.H) (hex : ∀ (s : ℝ), ∃ (j : Fin N), ⋯.eigenvalues j = Γ.lam s) (s : ℝ) : HasDerivAt Γ.Y ((deriv Γ.redRes s * deriv Γ.proj s + Γ.redRes s * deriv (deriv Γ.proj) s) * Γ.proj s + Γ.redRes s * deriv Γ.proj s * deriv Γ.proj s + ((deriv Γ.proj s * deriv Γ.proj s + Γ.proj s * deriv (deriv Γ.proj) s) * Γ.redRes s + Γ.proj s * deriv Γ.proj s * deriv Γ.redRes s)) s

Ẏ by the product rule.

The pointwise bounds

theorem Matrix.GappedPath.norm_deriv_proj_le {N : ℕ} (Γ : GappedPath N) {n : ℕ∞} (hn : 1 ≤ n) (hH : ContDiff ℝ (↑n) Γ.H) {s M₁ : ℝ} (hM₁ : 0 ≤ M₁) (h₁ : ‖deriv Γ.H s‖ ≤ M₁) : ‖deriv Γ.proj s‖ ≤ 2 * M₁ * (1 / Γ.g)

‖Ṗ‖ ≤ 2 M₁ / g.

theorem Matrix.GappedPath.norm_deriv_redRes_le {N : ℕ} (Γ : GappedPath N) {n : ℕ∞} (hn : 1 ≤ n) (hH : ContDiff ℝ (↑n) Γ.H) (hex : ∀ (s : ℝ), ∃ (j : Fin N), ⋯.eigenvalues j = Γ.lam s) {s M₁ : ℝ} (hM₁ : 0 ≤ M₁) (h₁ : ‖deriv Γ.H s‖ ≤ M₁) : ‖deriv Γ.redRes s‖ ≤ 6 * M₁ * (1 / Γ.g) ^ 2

‖Ẋ‖ ≤ 6 M₁ / g².

theorem Matrix.GappedPath.norm_deriv_deriv_proj_le {N : ℕ} (Γ : GappedPath N) {n : ℕ∞} (hn : 2 ≤ n) (hH : ContDiff ℝ (↑n) Γ.H) (hex : ∀ (s : ℝ), ∃ (j : Fin N), ⋯.eigenvalues j = Γ.lam s) {s M₁ M₂ : ℝ} (hM₁ : 0 ≤ M₁) (hM₂ : 0 ≤ M₂) (h₁ : ‖deriv Γ.H s‖ ≤ M₁) (h₂ : ‖deriv (deriv Γ.H) s‖ ≤ M₂) : ‖deriv (deriv Γ.proj) s‖ ≤ 16 * M₁ ^ 2 * (1 / Γ.g) ^ 2 + 2 * M₂ * (1 / Γ.g)

‖P̈‖ ≤ 16 M₁² / g² + 2 M₂ / g.

theorem Matrix.GappedPath.norm_Y_le {N : ℕ} (Γ : GappedPath N) {n : ℕ∞} (hn : 1 ≤ n) (hH : ContDiff ℝ (↑n) Γ.H) {s M₁ : ℝ} (hM₁ : 0 ≤ M₁) (h₁ : ‖deriv Γ.H s‖ ≤ M₁) : ‖Γ.Y s‖ ≤ 4 * M₁ * (1 / Γ.g) ^ 2

‖Y‖ ≤ 4 M₁ / g².

theorem Matrix.GappedPath.norm_K_le {N : ℕ} (Γ : GappedPath N) {n : ℕ∞} (hn : 1 ≤ n) (hH : ContDiff ℝ (↑n) Γ.H) {s M₁ : ℝ} (hM₁ : 0 ≤ M₁) (h₁ : ‖deriv Γ.H s‖ ≤ M₁) : ‖Γ.K s‖ ≤ 4 * M₁ * (1 / Γ.g)

‖K‖ ≤ 4 M₁ / g.

theorem Matrix.GappedPath.norm_deriv_Y_add_le {N : ℕ} (Γ : GappedPath N) {n : ℕ∞} (hn : 2 ≤ n) (hH : ContDiff ℝ (↑n) Γ.H) (hex : ∀ (s : ℝ), ∃ (j : Fin N), ⋯.eigenvalues j = Γ.lam s) {s M₁ M₂ : ℝ} (hM₁ : 0 ≤ M₁) (hM₂ : 0 ≤ M₂) (h₁ : ‖deriv Γ.H s‖ ≤ M₁) (h₂ : ‖deriv (deriv Γ.H) s‖ ≤ M₂) : ‖deriv Γ.Y s + Γ.Y s * Γ.K s‖ ≤ 80 * M₁ ^ 2 * (1 / Γ.g) ^ 3 + 4 * M₂ * (1 / Γ.g) ^ 2

‖Ẏ + Y K‖ ≤ 80 M₁² / g³ + 4 M₂ / g².

Kato's comparison with an explicit constant

theorem Matrix.GappedPath.norm_sub_le_explicit {N : ℕ} (Γ : GappedPath N) {n : ℕ∞} (hn : 2 ≤ n) (hH : ContDiff ℝ (↑n) Γ.H) (hex : ∀ (s : ℝ), ∃ (j : Fin N), ⋯.eigenvalues j = Γ.lam s) {M₁ M₂ : ℝ} (hM₁ : 0 ≤ M₁) (hM₂ : 0 ≤ M₂) (h₁ : ∀ s ∈ Set.Icc 0 1, ‖deriv Γ.H s‖ ≤ M₁) (h₂ : ∀ s ∈ Set.Icc 0 1, ‖deriv (deriv Γ.H) s‖ ≤ M₂) {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‖ ≤ (8 * M₁ / Γ.g ^ 2 + 4 * M₂ / Γ.g ^ 2 + 80 * M₁ ^ 2 / Γ.g ^ 3) / T

★★★ Kato's comparison with an explicit constant. Along a gapped C² path whose branch is an eigenvalue, with ‖Ḣ‖ ≤ M₁ and ‖Ḧ‖ ≤ M₂ on [0, 1], for every speed T > 0,

‖U_T(s) − U_A(s)‖ ≤ (8 M₁ / g² + 4 M₂ / g² + 80 M₁² / g³) / T on [0, 1].