The matrix propagator as an instance of the bounded-perturbation engine

Category: 1-Mathlib (CSD-free; staged for upstream).

The rule-of-two test of Analysis/Semigroup/BoundedPerturbation.lean (BACKLOG #40, FC-1′): the engine, instantiated on ℂᵐ with the free group S(t) = exp (t A) of a skew-Hermitian matrix A and the bounded perturbation B, must give back the matrix theorems of Analysis/Matrix/DysonSeries.lean and Analysis/Matrix/TrotterProduct.lean as corollaries. It does, and it gives them back with the skewness of B dropped: the matrix modules assumed Bᴴ = −B to keep every exponential factor unitary, the engine only needs B bounded.

• The dictionary. Matrix.toEuclideanCLM is an isometry for the L2 operator norm (cstar_norm_def is rfl), so it is continuous, commutes with exp (toEuclideanCLM_exp) and with interval integrals (toEuclideanCLM_mul_integral_apply); evalCLM ψ : M ↦ M ψ is the evaluation as a continuous linear map on matrices.
• expGroup A t = toEuclideanCLM (exp (t A)), a group; for Aᴴ = −A a group of contractions, so freeSemigroup A (the identity for t < 0) is an IsContractionSemigroup (isContractionSemigroup_freeSemigroup, through of_group).
• engine_dysonTerm_eq — the engine's Dyson terms are the matrix Dyson terms applied to ψ, Dₙ^{engine}(t) ψ = Dₙ(t) ψ, by the group law exp (t A) exp (−s A) = exp ((t − s) A) under the integral.
• ★ perturbed_eq_exp — the engine's perturbed semigroup is the matrix propagator, 𝒮(t) = exp (t (A + B)): the matrix Duhamel identity (exp_add_sub_exp_eq, the one analytic input) applied to ψ is the engine's Duhamel equation, and the engine's uniqueness (eq_dysonSum_of_duhamel) does the rest.
• ★★ hasSum_dysonTerm_of_engine — Matrix.hasSum_dysonTerm back from the engine, for any B: ∑ₙ Dₙ(t) = exp (t (A + B)) in the L2 operator norm; hasSum_dysonTerm_apply is the vector form.
• ★★ tendsto_trotter_of_engine — the matrix Trotter formula (exp ((t/n) A) exp ((t/n) B))ⁿ → exp (t (A + B)) from the engine's, for any B and 0 ≤ t; ★★ trotter_skew_of_engine is TrotterProduct.trotter_skew verbatim (t = 1), the engine's strong convergence upgraded to norm convergence by finite dimension (tendsto_of_forall_tendsto_apply).

Honest scope

⚠️ No rates. TrotterProduct.lean proves the O(1/n) rate; the engine's Trotter formula is a strong limit without a rate, so the rate is not recovered — only the limit. The matrix modules stay as they are; this module shows they are the engine's instance, it does not replace them.

References: Analysis/Semigroup/BoundedPerturbation.lean (FC-1); Analysis/Matrix/DysonSeries.lean, Analysis/Matrix/TrotterProduct.lean (row 36 (b)); specs/feynman-continuum-scoping.md §7 (the rule-of-two test named there); specs/BACKLOG.md #40; specs/future-work.md FP-1.

The dictionary

theorem Matrix.norm_toEuclideanCLM {m : Type u_1} [Fintype m] [DecidableEq m] (M : Matrix m m ℂ) : ‖toEuclideanCLM M‖ = ‖M‖

theorem Matrix.isometry_toEuclideanCLM {m : Type u_1} [Fintype m] [DecidableEq m] : Isometry ⇑toEuclideanCLM

theorem Matrix.continuous_toEuclideanCLM {m : Type u_1} [Fintype m] [DecidableEq m] : Continuous ⇑toEuclideanCLM

theorem Matrix.continuous_toEuclideanCLM_symm {m : Type u_1} [Fintype m] [DecidableEq m] : Continuous ⇑toEuclideanCLM.symm

theorem Matrix.toEuclideanCLM_exp {m : Type u_1} [Fintype m] [DecidableEq m] (M : Matrix m m ℂ) : toEuclideanCLM (NormedSpace.exp M) = NormedSpace.exp (toEuclideanCLM M)

toEuclideanCLM commutes with the exponential.

theorem Matrix.toEuclideanCLM_mul_apply {m : Type u_1} [Fintype m] [DecidableEq m] (M N : Matrix m m ℂ) (ψ : EuclideanSpace ℂ m) : (toEuclideanCLM (M * N)) ψ = (toEuclideanCLM M) ((toEuclideanCLM N) ψ)

noncomputable def Matrix.toEuclideanCLMₗ {m : Type u_1} [Fintype m] [DecidableEq m] : Matrix m m ℂ →L[ℂ] EuclideanSpace ℂ m →L[ℂ] EuclideanSpace ℂ m

toEuclideanCLM as a continuous linear map.

Equations

• Matrix.toEuclideanCLMₗ = Matrix.toEuclideanCLM.toAlgEquiv.toLinearMap.mkContinuous 1 ⋯

theorem Matrix.toEuclideanCLMₗ_apply {m : Type u_1} [Fintype m] [DecidableEq m] (M : Matrix m m ℂ) : toEuclideanCLMₗ M = toEuclideanCLM M

noncomputable def Matrix.evalCLM {m : Type u_1} [Fintype m] [DecidableEq m] (ψ : EuclideanSpace ℂ m) : Matrix m m ℂ →L[ℂ] EuclideanSpace ℂ m

Evaluation M ↦ M ψ as a continuous linear map on matrices.

Equations

• Matrix.evalCLM ψ = (ContinuousLinearMap.apply ℂ (EuclideanSpace ℂ m)) ψ ∘SL Matrix.toEuclideanCLMₗ

theorem Matrix.evalCLM_apply {m : Type u_1} [Fintype m] [DecidableEq m] (ψ : EuclideanSpace ℂ m) (M : Matrix m m ℂ) : (evalCLM ψ) M = (toEuclideanCLM M) ψ

theorem Matrix.opNorm_le_sum_norm_apply {m : Type u_1} [Fintype m] (T : EuclideanSpace ℂ m →L[ℂ] EuclideanSpace ℂ m) : ‖T‖ ≤ ∑ i : m, ‖T ((EuclideanSpace.basisFun m ℂ) i)‖

The operator norm on ℂᵐ is bounded by the sum of the norms of the images of the standard basis.

theorem Matrix.tendsto_of_forall_tendsto_apply {m : Type u_1} [Fintype m] [DecidableEq m] {ι : Type u_2} {l : Filter ι} {T : ι → Matrix m m ℂ} {L : Matrix m m ℂ} (h : ∀ (ψ : EuclideanSpace ℂ m), Filter.Tendsto (fun (i : ι) => (toEuclideanCLM (T i)) ψ) l (nhds ((toEuclideanCLM L) ψ))) : Filter.Tendsto T l (nhds L)

Strong convergence is norm convergence in finite dimension: a net of matrices converges in the L2 operator norm as soon as it converges on every vector.

The free group exp (t A) as a contraction semigroup

noncomputable def Matrix.expGroup {m : Type u_1} [Fintype m] [DecidableEq m] (A : Matrix m m ℂ) (t : ℝ) : EuclideanSpace ℂ m →L[ℂ] EuclideanSpace ℂ m

The one-parameter group t ↦ exp (t A) of a matrix A, as operators on ℂᵐ.

Equations

• A.expGroup t = Matrix.toEuclideanCLM (NormedSpace.exp (t • A))

theorem Matrix.expGroup_zero {m : Type u_1} [Fintype m] [DecidableEq m] (A : Matrix m m ℂ) : A.expGroup 0 = 1

theorem Matrix.expGroup_add {m : Type u_1} [Fintype m] [DecidableEq m] (A : Matrix m m ℂ) (s t : ℝ) : A.expGroup (s + t) = A.expGroup s * A.expGroup t

theorem Matrix.continuous_expGroup_apply {m : Type u_1} [Fintype m] [DecidableEq m] (A : Matrix m m ℂ) (ψ : EuclideanSpace ℂ m) : Continuous fun (t : ℝ) => (A.expGroup t) ψ

noncomputable def Matrix.freeSemigroup {m : Type u_1} [Fintype m] [DecidableEq m] (A : Matrix m m ℂ) (t : ℝ) : EuclideanSpace ℂ m →L[ℂ] EuclideanSpace ℂ m

The free semigroup exp (t A) for t ≥ 0, the identity for t < 0.

Equations

• A.freeSemigroup t = if 0 ≤ t then A.expGroup t else 1

theorem Matrix.freeSemigroup_of_nonneg {m : Type u_1} [Fintype m] [DecidableEq m] (A : Matrix m m ℂ) {t : ℝ} (ht : 0 ≤ t) : A.freeSemigroup t = A.expGroup t

The Dyson terms and the propagator

theorem Matrix.toEuclideanCLM_mul_integral_apply {m : Type u_1} [Fintype m] [DecidableEq m] (A : Matrix m m ℂ) {F : ℝ → Matrix m m ℂ} (hF : Continuous F) (s : ℝ) (ψ : EuclideanSpace ℂ m) : (toEuclideanCLM (NormedSpace.exp (s • A) * ∫ (r : ℝ) in 0..s, F r)) ψ = ∫ (r : ℝ) in 0..s, (toEuclideanCLM (NormedSpace.exp (s • A))) ((evalCLM ψ) (F r))

exp (s A) · ∫₀ˢ F, applied to ψ, is the integral of the operators applied to ψ.

theorem Matrix.expGroup_mul_apply {m : Type u_1} [Fintype m] [DecidableEq m] (A B M : Matrix m m ℂ) {r s : ℝ} (hrs : r ≤ s) (ψ : EuclideanSpace ℂ m) : (toEuclideanCLM (NormedSpace.exp (s • A))) ((evalCLM ψ) (NormedSpace.exp (-r • A) * B * M)) = (A.freeSemigroup (s - r)) ((toEuclideanCLM B) ((toEuclideanCLM M) ψ))

The kernel identity behind both Duhamel forms: for r ≤ s, exp (s A) · (exp (−r A) · B · M) ψ = S(s − r) (B (M ψ)).

theorem Matrix.continuous_dysonIntegrand {m : Type u_1} [Fintype m] [DecidableEq m] (A B : Matrix m m ℂ) (n : ℕ) : Continuous fun (s : ℝ) => NormedSpace.exp (-s • A) * B * A.dysonTerm B n s

theorem Matrix.engine_dysonTerm_eq {m : Type u_1} [Fintype m] [DecidableEq m] (A B : Matrix m m ℂ) (n : ℕ) {t : ℝ} : 0 ≤ t → ∀ (ψ : EuclideanSpace ℂ m), ContractionSemigroup.dysonTerm A.freeSemigroup (toEuclideanCLM B) n t ψ = (toEuclideanCLM (A.dysonTerm B n t)) ψ

The engine's Dyson terms are the matrix Dyson terms applied to ψ, for t ≥ 0.

theorem Matrix.exp_apply_eq_add_integral {m : Type u_1} [Fintype m] [DecidableEq m] (A B : Matrix m m ℂ) {t : ℝ} (ht : 0 ≤ t) (ψ : EuclideanSpace ℂ m) : (toEuclideanCLM (NormedSpace.exp (t • (A + B)))) ψ = (A.freeSemigroup t) ψ + ∫ (s : ℝ) in 0..t, (A.freeSemigroup (t - s)) ((toEuclideanCLM B) ((toEuclideanCLM (NormedSpace.exp (s • (A + B)))) ψ))

The matrix Duhamel identity, applied to ψ, is the engine's Duhamel equation.

theorem Matrix.trotterStep_eq {m : Type u_1} [Fintype m] [DecidableEq m] (A B : Matrix m m ℂ) {h : ℝ} (hh : 0 ≤ h) : ContractionSemigroup.trotterStep A.freeSemigroup (toEuclideanCLM B) h = toEuclideanCLM (NormedSpace.exp (h • A) * NormedSpace.exp (h • B))

The Trotter step of the engine is the matrix Trotter step exp (h A) · exp (h B).

The contraction semigroup, and the propagator

theorem Matrix.norm_expGroup_le {m : Type u_1} [Fintype m] [DecidableEq m] [Nonempty m] {A : Matrix m m ℂ} (hA : A.conjTranspose = -A) (t : ℝ) : ‖A.expGroup t‖ ≤ 1

theorem Matrix.isContractionSemigroup_freeSemigroup {m : Type u_1} [Fintype m] [DecidableEq m] [Nonempty m] {A : Matrix m m ℂ} (hA : A.conjTranspose = -A) : IsContractionSemigroup A.freeSemigroup

★ The unitary group of a skew-Hermitian matrix is a strongly continuous contraction semigroup in the sense of BoundedPerturbation.lean.

theorem Matrix.perturbed_eq_exp {m : Type u_1} [Fintype m] [DecidableEq m] [Nonempty m] {A : Matrix m m ℂ} (hA : A.conjTranspose = -A) (B : Matrix m m ℂ) {t : ℝ} (ht : 0 ≤ t) : ⋯.perturbed (toEuclideanCLM B) t = toEuclideanCLM (NormedSpace.exp (t • (A + B)))

★ The engine's perturbed semigroup is the matrix propagator: for Aᴴ = −A, any B and 0 ≤ t, the Dyson series of BoundedPerturbation.lean around exp (t A) with interaction B is exp (t (A + B)). The matrix Duhamel identity is the only analytic input; the engine's uniqueness theorem does the rest.

The matrix theorems, back from the engine

theorem Matrix.hasSum_dysonTerm_apply {m : Type u_1} [Fintype m] [DecidableEq m] [Nonempty m] {A : Matrix m m ℂ} (hA : A.conjTranspose = -A) (B : Matrix m m ℂ) {t : ℝ} (ht : 0 ≤ t) (ψ : EuclideanSpace ℂ m) : HasSum (fun (n : ℕ) => (toEuclideanCLM (A.dysonTerm B n t)) ψ) ((toEuclideanCLM (NormedSpace.exp (t • (A + B)))) ψ)

★★ The matrix Dyson series, vector form, from the engine: for Aᴴ = −A, any B and 0 ≤ t, ∑ₙ Dₙ(t) ψ = exp (t (A + B)) ψ.

theorem Matrix.hasSum_dysonTerm_of_engine {m : Type u_1} [Fintype m] [DecidableEq m] [Nonempty m] {A : Matrix m m ℂ} (hA : A.conjTranspose = -A) (B : Matrix m m ℂ) {t : ℝ} (ht : 0 ≤ t) : HasSum (fun (n : ℕ) => A.dysonTerm B n t) (NormedSpace.exp (t • (A + B)))

★★ Matrix.hasSum_dysonTerm, back from the engine — and for any B: for Aᴴ = −A and 0 ≤ t, ∑ₙ Dₙ(t) = exp (t (A + B)) in the L2 operator norm. The engine's term bound gives summability in operator norm; the vector form identifies the sum.

theorem Matrix.tendsto_trotter_apply {m : Type u_1} [Fintype m] [DecidableEq m] [Nonempty m] {A : Matrix m m ℂ} (hA : A.conjTranspose = -A) (B : Matrix m m ℂ) {t : ℝ} (ht : 0 ≤ t) (ψ : EuclideanSpace ℂ m) : Filter.Tendsto (fun (n : ℕ) => (toEuclideanCLM ((NormedSpace.exp ((t / ↑n) • A) * NormedSpace.exp ((t / ↑n) • B)) ^ n)) ψ) Filter.atTop (nhds ((toEuclideanCLM (NormedSpace.exp (t • (A + B)))) ψ))

★★ The matrix Trotter formula, vector form, from the engine: for Aᴴ = −A, any B and 0 ≤ t, (exp ((t/n) A) · exp ((t/n) B))ⁿ ψ → exp (t (A + B)) ψ.

theorem Matrix.tendsto_trotter_of_engine {m : Type u_1} [Fintype m] [DecidableEq m] [Nonempty m] {A : Matrix m m ℂ} (hA : A.conjTranspose = -A) (B : Matrix m m ℂ) {t : ℝ} (ht : 0 ≤ t) : Filter.Tendsto (fun (n : ℕ) => (NormedSpace.exp ((t / ↑n) • A) * NormedSpace.exp ((t / ↑n) • B)) ^ n) Filter.atTop (nhds (NormedSpace.exp (t • (A + B))))

★★ The matrix Trotter formula, from the engine — and for any B: for Aᴴ = −A and 0 ≤ t, (exp ((t/n) A) · exp ((t/n) B))ⁿ → exp (t (A + B)) in the L2 operator norm.

theorem Matrix.trotter_skew_of_engine {m : Type u_1} [Fintype m] [DecidableEq m] [Nonempty m] {A : Matrix m m ℂ} (hA : A.conjTranspose = -A) (B : Matrix m m ℂ) : Filter.Tendsto (fun (n : ℕ) => (NormedSpace.exp ((↑n)⁻¹ • A) * NormedSpace.exp ((↑n)⁻¹ • B)) ^ n) Filter.atTop (nhds (NormedSpace.exp (A + B)))

★★ TrotterProduct.trotter_skew back from the engine, verbatim (t = 1), with the skewness of B no longer needed: (exp (A/n) · exp (B/n))ⁿ → exp (A + B).