The Riesz projector along a gapped path: smoothness and P Ṗ P = 0

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

A gapped path (GappedPath N) is a family H s of Hermitian matrices with a continuous eigenvalue branch lam s isolated from the rest of the spectrum by a gap g > 0, uniformly in s. Its eigenprojector proj s is the Riesz projector of H s over the disc of radius g/2 about lam s (RieszProjector.lean). This file proves that proj is as smooth as H, and the identity P Ṗ P = 0 that Kato's intertwiner (#160) is built on.

• HasDerivAt.eq_mul_add_mul_of_idempotent, ★ HasDerivAt.mul_deriv_mul_eq_zero_of_idempotent — an idempotent C¹ family has Ṗ = ṖP + PṖ and P Ṗ P = 0: differentiate P² = P and sandwich. Any normed algebra.
• resolventIntegrand, rieszProj_eq_integral, rieszProj_eq_integral_unit — the Riesz projector as an interval integral over [0, 1] of the resolvent on the circle;
• contDiffOn_inv_comp, ★ contDiffOn_circleIntegral — the matrix inverse is C^n on units, and a parametric circle integral of a jointly C^n integrand is C^n (the general form, used again for the reduced resolvent in #162);
• ★★ contDiffOn_rieszProj — over a fixed contour the Riesz projector is C^n in the matrix path: the integrand is C^n jointly (the inverse is C^n on units, contDiffAt_ringInverse; the units form an open set, Units.isOpen), and a parametric interval integral of a jointly C^n integrand is C^n (contDiffOn_intervalIntegral_of_contDiffOn, generalised from ℝ to a normed codomain for this file);
• GappedPath.proj_eq_near — the contour can be frozen locally: for |lam s − lam s₀| < g/4 the disc about lam s₀ isolates the same eigenvalue, so proj s is the integral over the fixed circle about lam s₀;
• ★★ GappedPath.contDiff_proj — proj is C^n whenever H is, by the two previous items;
• GappedPath.deriv_proj_eq, ★ GappedPath.proj_mul_deriv_mul_proj — Ṗ = ṖP + PṖ and P Ṗ P = 0 along the path;
• GappedPath.proj_mul_self, proj_isHermitian, H_mul_proj / proj_mul_H (H P = lam • P), trace_proj (the trace is the multiplicity), ★ mult_eq (the multiplicity is constant, by continuity of the trace into ℕ), ★ contDiff_lam — the eigenvalue branch is C^n whenever H is, as lam s = tr(H s · P s) / mult; so the continuity of lam assumed in GappedPath is all the regularity it ever needs.

Honest scope

• Finite dimensions, Fin N, 𝕜 = ℂ, the L2Operator norm scope throughout: the hypothesis ContDiff ℝ n H is smoothness into the matrix space with the operator norm (in finite dimensions this is entrywise smoothness, but no transfer lemma is used or needed here).
• The gap is uniform in s and the branch is given; nothing is said about eigenvalue crossings.
• contDiffOn_rieszProj asks for the circle to avoid the spectrum on an open set of parameters; openness of that set is NOT derived from continuity of eigenvalues (not in Mathlib) but supplied by the gap, through proj_eq_near.

References: T. Kato, Perturbation Theory for Linear Operators, II §1.4, §5.4; Kato 1950; S. Teufel, Adiabatic Perturbation Theory in Quantum Dynamics, §2.1; RieszProjector.lean (#158), Analysis/Calculus/ContDiffParametricIntervalIntegral.lean (#60); specs/BACKLOG.md #159, #88.

An idempotent C¹ family: P Ṗ P = 0

theorem HasDerivAt.eq_mul_add_mul_of_idempotent {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {A : Type u_2} [NormedRing A] [NormedAlgebra 𝕜 A] {P : 𝕜 → A} {P' : A} {s : 𝕜} (hP : ∀ (t : 𝕜), P t * P t = P t) (hd : HasDerivAt P P' s) : P' = P' * P s + P s * P'

★ An idempotent C¹ family has P Ṗ P = 0. If P t * P t = P t for all t and P has derivative P' at s, then P s * P' * P s = 0: differentiating P² = P gives P' = P' P + P P', and sandwiching with P gives P P' P = 2 P P' P.

theorem HasDerivAt.mul_deriv_mul_eq_zero_of_idempotent {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {A : Type u_2} [NormedRing A] [NormedAlgebra 𝕜 A] {P : 𝕜 → A} {P' : A} {s : 𝕜} (hP : ∀ (t : 𝕜), P t * P t = P t) (hd : HasDerivAt P P' s) : P s * P' * P s = 0

Complex scalars on matrices, smoothly

theorem Matrix.contDiff_smul_of_contDiff {N : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : WithTop ℕ∞} {f : E → ℂ} {g : E → Matrix (Fin N) (Fin N) ℂ} (hf : ContDiff ℝ n f) (hg : ContDiff ℝ n g) : ContDiff ℝ n fun (x : E) => f x • g x

ℂ-scalar multiplication on matrices is C^n in both arguments, over ℝ.

theorem Matrix.contDiffOn_smul_of_contDiffOn {N : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : WithTop ℕ∞} {f : E → ℂ} {g : E → Matrix (Fin N) (Fin N) ℂ} {s : Set E} (hf : ContDiffOn ℝ n f s) (hg : ContDiffOn ℝ n g s) : ContDiffOn ℝ n (fun (x : E) => f x • g x) s

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

The trace as a continuous ℝ-linear map.

Equations

• Matrix.traceCLM = LinearMap.toContinuousLinearMap (↑ℝ (Matrix.traceLinearMap (Fin N) ℂ ℂ))

@[simp]

theorem Matrix.traceCLM_apply {N : ℕ} (A : Matrix (Fin N) (Fin N) ℂ) : traceCLM A = A.trace

The Riesz projector over a fixed contour is smooth in the matrix

noncomputable def Matrix.resolventIntegrand {N : ℕ} (c : ℂ) (r : ℝ) (A : Matrix (Fin N) (Fin N) ℂ) (θ : ℝ) : Matrix (Fin N) (Fin N) ℂ

The resolvent integrand on the circle C(c, r): (r i e^{iθ}) • (circleMap c r θ • 1 − A)⁻¹, with the inverse written as Ring.inverse so that its smoothness on units is Mathlib's.

Equations

• Matrix.resolventIntegrand c r A θ = (circleMap 0 r θ * Complex.I) • Ring.inverse (circleMap c r θ • 1 - A)

theorem Matrix.rieszProj_eq_integral {N : ℕ} (A : Matrix (Fin N) (Fin N) ℂ) (c : ℂ) (r : ℝ) : A.rieszProj c r = (2 * ↑Real.pi * Complex.I)⁻¹ • ∫ (θ : ℝ) in 0..2 * Real.pi, resolventIntegrand c r A θ

The Riesz projector as an interval integral over [0, 2π].

theorem Matrix.rieszProj_eq_integral_unit {N : ℕ} (A : Matrix (Fin N) (Fin N) ℂ) (c : ℂ) (r : ℝ) : A.rieszProj c r = (2 * ↑Real.pi * Complex.I)⁻¹ • (2 * Real.pi) • ∫ (u : ℝ) in 0..1, resolventIntegrand c r A (2 * Real.pi * u)

The Riesz projector as an interval integral over [0, 1].

theorem Matrix.contDiffOn_inv_comp {N : ℕ} {n : ℕ∞} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Φ : E → Matrix (Fin N) (Fin N) ℂ} (hΦ : ContDiff ℝ (↑n) Φ) {W : Set E} (hW : ∀ p ∈ W, IsUnit (Φ p)) : ContDiffOn ℝ (↑n) (fun (p : E) => (Φ p)⁻¹) W

Composition with the matrix inverse is C^n where the matrix is a unit.

theorem Matrix.contDiffOn_circleIntegral {N : ℕ} {n : ℕ∞} {F : ℝ → ℂ → Matrix (Fin N) (Fin N) ℂ} {V : Set ℝ} (hV : IsOpen V) (c : ℂ) (r : ℝ) {W : Set (ℝ × ℝ)} (hW : IsOpen W) (hVW : ∀ s ∈ V, ∀ u ∈ Set.Icc 0 1, (s, u) ∈ W) (hF : ContDiffOn ℝ (↑n) (fun (p : ℝ × ℝ) => F p.1 (circleMap c r (2 * Real.pi * p.2))) W) : ContDiffOn ℝ (↑n) (fun (s : ℝ) => ∮ (z : ℂ) in C(c, r), F s z) V

★ A parametric circle integral of a jointly C^n matrix-valued integrand is C^n in the parameter: if (s, u) ↦ F s (circleMap c r (2πu)) is C^n on an open W ⊇ V × [0, 1], then s ↦ ∮_{C(c, r)} F s z dz is C^n on the open V.

theorem Matrix.contDiffOn_rieszProj {N : ℕ} {n : ℕ∞} {H : ℝ → Matrix (Fin N) (Fin N) ℂ} (hH : ContDiff ℝ (↑n) H) {V : Set ℝ} (hV : IsOpen V) {c : ℂ} {r : ℝ} (hr : 0 ≤ r) (hu : ∀ s ∈ V, ∀ z ∈ Metric.sphere c r, IsUnit (z • 1 - H s)) : ContDiffOn ℝ (↑n) (fun (s : ℝ) => (H s).rieszProj c r) V

★★ Over a fixed contour the Riesz projector is C^n in the matrix path. If H is C^n and, for every parameter in the open set V, no point of the circle C(c, r) is in the spectrum of H s, then s ↦ rieszProj (H s) c r is C^n on V.

Gapped paths

structure Matrix.GappedPath (N : ℕ) : Type

A gapped path of Hermitian matrices: a continuous eigenvalue branch lam isolated by a gap g > 0 from the rest of the spectrum, uniformly in the parameter.

• H : ℝ → Matrix (Fin N) (Fin N) ℂ

  The path of Hermitian matrices.

• isHermitian (s : ℝ) : (self.H s).IsHermitian
• lam : ℝ → ℝ

  The eigenvalue branch.

• continuous_lam : Continuous self.lam
• g : ℝ

  The gap.

• g_pos : 0 < self.g
• gap (s : ℝ) (j : Fin N) : ⋯.eigenvalues j = self.lam s ∨ self.g ≤ |⋯.eigenvalues j - self.lam s|

  Every eigenvalue is either on the branch or at distance at least g from it.

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

The eigenprojector of the branch: the Riesz projector of H s over the disc of radius g/2 about lam s.

Equations

• Γ.proj s = (Γ.H s).rieszProj (↑(Γ.lam s)) (Γ.g / 2)

noncomputable def Matrix.GappedPath.mult {N : ℕ} (Γ : GappedPath N) (s : ℝ) : ℕ

The multiplicity of the branch at s.

Equations

• Γ.mult s = Fintype.card { j : Fin N // ⋯.eigenvalues j = Γ.lam s }

theorem Matrix.GappedPath.dist_eigC {N : ℕ} (Γ : GappedPath N) (s : ℝ) (j : Fin N) (x : ℝ) : dist (⋯.eigC j) ↑x = |⋯.eigenvalues j - x|

theorem Matrix.GappedPath.hcirc_self {N : ℕ} (Γ : GappedPath N) (s : ℝ) (j : Fin N) : dist (⋯.eigC j) ↑(Γ.lam s) ≠ Γ.g / 2

The circle about lam s of radius g/2 avoids the spectrum of H s.

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

For |lam s − lam s₀| < g/4, the circle about lam s₀ of radius g/2 avoids the spectrum of H s as well.

theorem Matrix.GappedPath.discInd_eq {N : ℕ} (Γ : GappedPath N) (s : ℝ) (j : Fin N) : ⋯.discInd (↑(Γ.lam s)) (Γ.g / 2) j = if ⋯.eigenvalues j = Γ.lam s then 1 else 0

The indicator of the disc about lam s is the indicator of the branch.

theorem Matrix.GappedPath.discInd_eq_near {N : ℕ} (Γ : GappedPath N) {s s₀ : ℝ} (h : |Γ.lam s - Γ.lam s₀| < Γ.g / 4) : ⋯.discInd (↑(Γ.lam s)) (Γ.g / 2) = ⋯.discInd (↑(Γ.lam s₀)) (Γ.g / 2)

For |lam s − lam s₀| < g/4, the discs about lam s and lam s₀ select the same eigenvalues of H s.

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

The contour can be frozen locally: for |lam s − lam s₀| < g/4, proj s is the Riesz projector of H s over the fixed disc about lam s₀.

theorem Matrix.GappedPath.isUnit_smul_one_sub {N : ℕ} (Γ : GappedPath N) {s : ℝ} {z : ℂ} (hz : ∀ (j : Fin N), z ≠ ⋯.eigC j) : IsUnit (z • 1 - Γ.H s)

Off the spectrum, z • 1 − H s is a unit.

theorem Matrix.GappedPath.contDiff_proj {N : ℕ} (Γ : GappedPath N) {n : ℕ∞} (hH : ContDiff ℝ (↑n) Γ.H) : ContDiff ℝ (↑n) Γ.proj

★★ The eigenprojector is C^n whenever the path is.

The algebra of the eigenprojector

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

theorem Matrix.GappedPath.proj_isHermitian {N : ℕ} (Γ : GappedPath N) (s : ℝ) : (Γ.proj s).IsHermitian

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

H s · P s = lam s • P s.

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

P s · H s = lam s • P s.

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

The eigenprojector has derivative deriv Γ.proj s at s once the path is C¹.

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

Ṗ = Ṗ P + P Ṗ along a gapped C¹ path.

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

★ P Ṗ P = 0 along a gapped C¹ path.

The multiplicity is constant, and the branch is smooth

theorem Matrix.IsHermitian.trace_conjD {N : ℕ} {H : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) (d : Fin N → ℂ) : (hH.conjD d).trace = ∑ j : Fin N, d j

theorem Matrix.GappedPath.trace_proj {N : ℕ} (Γ : GappedPath N) (s : ℝ) : (Γ.proj s).trace = ↑(Γ.mult s)

The trace of the eigenprojector is the multiplicity of the branch.

theorem Nat.eq_of_dist_cast_lt_one {a b : ℕ} (h : dist ↑a ↑b < 1) : a = b

Two naturals whose real casts are within 1 are equal.

theorem Matrix.GappedPath.mult_eq {N : ℕ} (Γ : GappedPath N) {n : ℕ∞} (hH : ContDiff ℝ (↑n) Γ.H) (s t : ℝ) : Γ.mult s = Γ.mult t

★ The multiplicity of the branch is constant along the path.

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

theorem Matrix.GappedPath.ofReal_lam_eq {N : ℕ} (Γ : GappedPath N) {s : ℝ} (hex : ∃ (j : Fin N), ⋯.eigenvalues j = Γ.lam s) : ↑(Γ.lam s) = (Γ.H s * Γ.proj s).trace / ↑(Γ.mult s)

lam s = tr(H s · P s) / mult s once the branch is an eigenvalue.

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

★ The eigenvalue branch is C^n whenever the path is, provided it is an eigenvalue: lam s = tr(H s · P s) / mult, with the multiplicity constant.