The Dyson series of a perturbed unitary group

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

For skew-Hermitian generators A (free) and B (interaction) on a finite-dimensional Hilbert space, the propagator exp (t (A + B)) is the sum of the Dyson series

exp (t (A + B)) = ∑ₙ Dₙ(t), D₀(t) = exp (t A), Dₙ₊₁(t) = exp (t A) · ∫₀ᵗ exp (−s A) · B · Dₙ(s) ds,

the interaction-picture expansion in powers of the interaction. Each term is a primitive of a continuous matrix-valued function, so the whole construction is ordinary Bochner integration on Matrix m m ℂ under the L2 operator norm; the exponentials of the skew-Hermitian generators are unitary, so every norm bound is free of growth factors, as in TrotterProduct.lean and DuhamelBound.lean.

• dysonTerm A B n t — the n-th term, dysonTerm_zero, dysonTerm_succ; continuous_dysonTerm — each term is continuous in t;
• ★ norm_dysonTerm_le — ‖Dₙ(t)‖ ≤ (‖B‖ t)ⁿ / n! for 0 ≤ t;
• ★ exp_add_sub_exp_eq — the Duhamel identity, exp (t (A + B)) − exp (t A) = exp (t A) · ∫₀ᵗ exp (−s A) · B · exp (s (A + B)) ds, by the fundamental theorem of calculus on the interpolant exp (−s A) · exp (s (A + B));
• dysonRemainder A B n t = exp (t (A + B)) − ∑_{k < n} Dₖ(t), with ★ dysonRemainder_succ — the remainder satisfies the same Volterra recursion as the terms, and ★ norm_dysonRemainder_le — the truncation error, ‖Rₙ(t)‖ ≤ (‖B‖ t)ⁿ / n!;
• ★★ hasSum_dysonTerm — the Dyson series converges to the propagator, HasSum (fun n => Dₙ(t)) (exp (t (A + B))), and summable_dysonTerm;
• ★★ hasSum_dysonTerm_of_isHermitian — the same for a Hamiltonian H₀ + V split into two Hermitian parts, generators −i H₀ and −i V: the propagator exp (−i t (H₀ + V)) is the sum of the Dyson series in powers of V.

Honest scope

⚠️ Finite dimension, forward time. The bounds and the convergence are stated for 0 ≤ t (the identities hold for every t). The exponentials are matrix exponentials; nothing here concerns unbounded generators.

⚠️ Skew-Hermitian generators. Skewness is used exactly once per bound, to give the exponential factors norm one. The recursion and the Duhamel identity hold for arbitrary A, B; the general bound would carry exp (t ‖A‖), as TrotterGeneral.lean de-skews the product formula.

References: F. J. Dyson, The radiation theories of Tomonaga, Schwinger, and Feynman, Phys. Rev. 75, 486 (1949); Analysis/Matrix/DuhamelBound.lean (the interpolant and l2_opNorm_exp_smul_skew); Analysis/Matrix/SumOverPaths.lean (rung (a) of the same programme); specs/BACKLOG.md #36(b); specs/future-work.md.

The terms

noncomputable def Matrix.dysonTerm {m : Type u_1} [Fintype m] [DecidableEq m] (A B : Matrix m m ℂ) : ℕ → ℝ → Matrix m m ℂ

The Dyson terms in the interaction picture: D₀(t) = exp (t A) and Dₙ₊₁(t) = exp (t A) · ∫₀ᵗ exp (−s A) · B · Dₙ(s) ds.

Equations

• A.dysonTerm B 0 = fun (t : ℝ) => NormedSpace.exp (t • A)
• A.dysonTerm B n.succ = fun (t : ℝ) => NormedSpace.exp (t • A) * ∫ (s : ℝ) in 0..t, NormedSpace.exp (-s • A) * B * A.dysonTerm B n s

theorem Matrix.dysonTerm_zero {m : Type u_1} [Fintype m] [DecidableEq m] (A B : Matrix m m ℂ) (t : ℝ) : A.dysonTerm B 0 t = NormedSpace.exp (t • A)

theorem Matrix.dysonTerm_succ {m : Type u_1} [Fintype m] [DecidableEq m] (A B : Matrix m m ℂ) (n : ℕ) (t : ℝ) : A.dysonTerm B (n + 1) t = NormedSpace.exp (t • A) * ∫ (s : ℝ) in 0..t, NormedSpace.exp (-s • A) * B * A.dysonTerm B n s

theorem Matrix.continuous_exp_smul {m : Type u_1} [Fintype m] [DecidableEq m] (A : Matrix m m ℂ) : Continuous fun (t : ℝ) => NormedSpace.exp (t • A)

theorem Matrix.continuous_exp_neg_smul {m : Type u_1} [Fintype m] [DecidableEq m] (A : Matrix m m ℂ) : Continuous fun (t : ℝ) => NormedSpace.exp (-t • A)

theorem Matrix.continuous_dysonTerm {m : Type u_1} [Fintype m] [DecidableEq m] (A B : Matrix m m ℂ) (n : ℕ) : Continuous (A.dysonTerm B n)

Each Dyson term is continuous in time.

The bound on the terms

theorem Matrix.norm_dysonTerm_le {m : Type u_1} [Fintype m] [DecidableEq m] [Nonempty m] {A : Matrix m m ℂ} (hA : A.conjTranspose = -A) (B : Matrix m m ℂ) (n : ℕ) {t : ℝ} (ht : 0 ≤ t) : ‖A.dysonTerm B n t‖ ≤ (‖B‖ * t) ^ n / ↑n.factorial

★ ‖Dₙ(t)‖ ≤ (‖B‖ t)ⁿ / n! for 0 ≤ t and skew-Hermitian A.

The Duhamel identity and the remainder

theorem Matrix.hasDerivAt_exp_neg_smul_mul_exp_smul_add {m : Type u_1} [Fintype m] [DecidableEq m] (A B : Matrix m m ℂ) (s : ℝ) : HasDerivAt (fun (u : ℝ) => NormedSpace.exp (-u • A) * NormedSpace.exp (u • (A + B))) (NormedSpace.exp (-s • A) * B * NormedSpace.exp (s • (A + B))) s

The interpolant s ↦ exp (−s A) · exp (s (A + B)) has derivative exp (−s A) · B · exp (s (A + B)).

theorem Matrix.exp_add_sub_exp_eq {m : Type u_1} [Fintype m] [DecidableEq m] (A B : Matrix m m ℂ) (t : ℝ) : NormedSpace.exp (t • (A + B)) - NormedSpace.exp (t • A) = NormedSpace.exp (t • A) * ∫ (s : ℝ) in 0..t, NormedSpace.exp (-s • A) * B * NormedSpace.exp (s • (A + B))

★ The Duhamel identity. exp (t (A + B)) − exp (t A) = exp (t A) · ∫₀ᵗ exp (−s A) · B · exp (s (A + B)) ds.

noncomputable def Matrix.dysonRemainder {m : Type u_1} [Fintype m] [DecidableEq m] (A B : Matrix m m ℂ) (n : ℕ) (t : ℝ) : Matrix m m ℂ

The remainder after n terms: Rₙ(t) = exp (t (A + B)) − ∑_{k < n} Dₖ(t).

Equations

• A.dysonRemainder B n t = NormedSpace.exp (t • (A + B)) - ∑ k ∈ Finset.range n, A.dysonTerm B k t

theorem Matrix.dysonRemainder_zero {m : Type u_1} [Fintype m] [DecidableEq m] (A B : Matrix m m ℂ) (t : ℝ) : A.dysonRemainder B 0 t = NormedSpace.exp (t • (A + B))

theorem Matrix.continuous_dysonRemainder {m : Type u_1} [Fintype m] [DecidableEq m] (A B : Matrix m m ℂ) (n : ℕ) : Continuous (A.dysonRemainder B n)

The remainder is continuous in time.

theorem Matrix.dysonRemainder_succ {m : Type u_1} [Fintype m] [DecidableEq m] (A B : Matrix m m ℂ) (n : ℕ) (t : ℝ) : A.dysonRemainder B (n + 1) t = NormedSpace.exp (t • A) * ∫ (s : ℝ) in 0..t, NormedSpace.exp (-s • A) * B * A.dysonRemainder B n s

★ The remainder obeys the Volterra recursion of the terms: Rₙ₊₁(t) = exp (t A) · ∫₀ᵗ exp (−s A) · B · Rₙ(s) ds.

theorem Matrix.norm_dysonRemainder_le {m : Type u_1} [Fintype m] [DecidableEq m] [Nonempty m] {A B : Matrix m m ℂ} (hA : A.conjTranspose = -A) (hB : B.conjTranspose = -B) (n : ℕ) {t : ℝ} (ht : 0 ≤ t) : ‖A.dysonRemainder B n t‖ ≤ (‖B‖ * t) ^ n / ↑n.factorial

★ The truncation error: ‖Rₙ(t)‖ ≤ (‖B‖ t)ⁿ / n! for 0 ≤ t and skew-Hermitian A, B.

Convergence

theorem Matrix.summable_dysonTerm {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) : Summable fun (n : ℕ) => A.dysonTerm B n t

The Dyson terms are summable.

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

★★ The Dyson series converges to the propagator: for skew-Hermitian A, B and 0 ≤ t, ∑ₙ Dₙ(t) = exp (t (A + B)).

theorem Matrix.conjTranspose_neg_I_smul_of_isHermitian {m : Type u_1} {H : Matrix m m ℂ} (hH : H.IsHermitian) : (-Complex.I • H).conjTranspose = -(-Complex.I • H)

For Hermitian H, the generator −i H is skew-Hermitian.

theorem Matrix.hasSum_dysonTerm_of_isHermitian {m : Type u_1} [Fintype m] [DecidableEq m] [Nonempty m] {H₀ V : Matrix m m ℂ} (h₀ : H₀.IsHermitian) (hV : V.IsHermitian) {t : ℝ} (ht : 0 ≤ t) : HasSum (fun (n : ℕ) => (-Complex.I • H₀).dysonTerm (-Complex.I • V) n t) (NormedSpace.exp (t • -Complex.I • (H₀ + V)))

★★ The Dyson series of a split Hamiltonian. For Hermitian H₀ and V and 0 ≤ t, the propagator exp (−i t (H₀ + V)) is the sum of the Dyson series with free generator −i H₀ and interaction −i V: the expansion in powers of the interaction.