The vertex bookkeeping of the Dyson series

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

DysonSeries.lean expands the propagator exp (t (A + B)) in powers of the interaction B. This module is the bookkeeping that turns the n-th term into a sum over diagrams with n vertices: the interaction picture, the ordered vertex times, the labelling of the vertices when the interaction is a sum of vertex types, and — in the eigenbasis of a diagonal free generator — the old-fashioned (time-ordered) perturbation theory with intermediate states and its explicit first- and second-order amplitudes.

• interactionPicture A B s = exp (−s A) · B · exp (s A) — the interaction-picture vertex; dysonTermI A B n t = exp (−t A) · Dₙ(t) — the term in the interaction picture, with dysonTermI_zero (= 1) and ★ dysonTermI_succ, dysonTermI (n + 1) t = ∫₀ᵗ V_I(s) · dysonTermI n s ds: unrolled, the n-th term is the time-ordered product ∫_{0 ≤ s₁ ≤ ⋯ ≤ sₙ ≤ t} V_I(sₙ) ⋯ V_I(s₁) ds — the n vertices at ordered times, dysonTerm_eq_exp_smul_mul_dysonTermI;
• dysonTermLabelled A B n f t — the term with the vertex type f i at slot i (f 0 the latest), and ★ dysonTerm_sum_eq_sum_dysonTermLabelled — the sum over labellings: for an interaction ∑ v, B v (a sum of vertex types — local vertices at the sites of a lattice, the monomials of a polynomial interaction), the n-th term is the sum over all f : Fin n → ι of the labelled terms, one per assignment of a type to each of the n ordered vertices;
• intervalIntegral_apply — the entry of a matrix-valued interval integral is the interval integral of the entry;
• Diagonal free generator A = diagonal a (the eigenbasis; a i = −i Eᵢ for a Hamiltonian): interactionPicture_diagonal_apply — V_I(s) i j = e^{s (aⱼ − aᵢ)} · B i j, the vertex dressed with the free phases of its two legs; ★ dysonTermI_succ_apply_diagonal — old-fashioned perturbation theory, one vertex at a time: dysonTermI (n + 1) t i j = ∫₀ᵗ ∑ₖ e^{s (aₖ − aᵢ)} B i k · dysonTermI n s k j ds, the sum over the intermediate state k after the latest vertex; dysonTermI_one_apply_diagonal, ★ dysonTerm_one_apply_diagonal_self (D₁(t) i i = e^{t aᵢ} · t · B i i, the first-order diagonal amplitude — with B a polynomial in the field, the one-vertex vacuum diagram), ★ dysonTerm_one_apply_diagonal_of_ne (D₁(t) i j = B i j · (e^{t aⱼ} − e^{t aᵢ}) / (aⱼ − aᵢ), the first-order transition amplitude of time-dependent perturbation theory), and ★ dysonTermI_two_apply_diagonal / dysonTermI_two_apply_diagonal_self — the two-vertex amplitude as the double integral over 0 ≤ s₁ ≤ s₂ ≤ t of the sum over the intermediate state of the two vertex entries dressed with the free propagation between them.

Honest scope

⚠️ Bookkeeping only. Nothing here evaluates a vacuum expectation: the reduction of ⟨V_I(sₙ) ⋯ V_I(s₁)⟩ to a sum over pairings of propagators is Wick's theorem, which lives with the field (the CSD lattice's CV/Wick.lean, CV/WickGeneral.lean) and is joined to these identities in CV/FeynmanVertex.lean. The 1/n! of the unordered-time form is not stated: the terms are kept as ordered (simplex) integrals, which is what the recursion gives.

⚠️ Finite dimension. Matrix exponentials and Bochner integrals of matrices under the L2 operator norm, as in DysonSeries.lean; no unbounded generators.

References: F. J. Dyson, The radiation theories of Tomonaga, Schwinger, and Feynman, Phys. Rev. 75, 486 (1949) §III (the time-ordered expansion); Analysis/Matrix/DysonSeries.lean; specs/BACKLOG.md #36(b)(iii); specs/future-work.md.

Entries of matrix-valued integrals

theorem Matrix.intervalIntegral_apply {m : Type u_1} [Fintype m] [DecidableEq m] {f : ℝ → Matrix m m ℂ} {a b : ℝ} (hf : IntervalIntegrable f MeasureTheory.volume a b) (i j : m) : (∫ (s : ℝ) in a..b, f s) i j = ∫ (s : ℝ) in a..b, f s i j

The (i, j) entry of a matrix-valued interval integral is the interval integral of the entry.

theorem Matrix.exp_neg_smul_mul_exp_smul {m : Type u_1} [Fintype m] [DecidableEq m] (A : Matrix m m ℂ) (t : ℝ) : NormedSpace.exp (-t • A) * NormedSpace.exp (t • A) = 1

theorem Matrix.exp_smul_mul_exp_neg_smul {m : Type u_1} [Fintype m] [DecidableEq m] (A : Matrix m m ℂ) (t : ℝ) : NormedSpace.exp (t • A) * NormedSpace.exp (-t • A) = 1

The interaction picture

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

The interaction-picture vertex V_I(s) = exp (−s A) · B · exp (s A): the interaction transported by the free evolution to time s.

Equations

• A.interactionPicture B s = NormedSpace.exp (-s • A) * B * NormedSpace.exp (s • A)

theorem Matrix.continuous_interactionPicture {m : Type u_1} [Fintype m] [DecidableEq m] (A B : Matrix m m ℂ) : Continuous (A.interactionPicture B)

theorem Matrix.interactionPicture_smul {m : Type u_1} [Fintype m] [DecidableEq m] (A B : Matrix m m ℂ) (c : ℂ) (s : ℝ) : A.interactionPicture (c • B) s = c • A.interactionPicture B s

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

The Dyson term in the interaction picture, exp (−t A) · Dₙ(t).

Equations

• A.dysonTermI B n t = NormedSpace.exp (-t • A) * A.dysonTerm B n t

theorem Matrix.dysonTerm_eq_exp_smul_mul_dysonTermI {m : Type u_1} [Fintype m] [DecidableEq m] (A B : Matrix m m ℂ) (n : ℕ) (t : ℝ) : A.dysonTerm B n t = NormedSpace.exp (t • A) * A.dysonTermI B n t

theorem Matrix.dysonTermI_zero {m : Type u_1} [Fintype m] [DecidableEq m] (A B : Matrix m m ℂ) (t : ℝ) : A.dysonTermI B 0 t = 1

theorem Matrix.dysonTermI_succ {m : Type u_1} [Fintype m] [DecidableEq m] (A B : Matrix m m ℂ) (n : ℕ) (t : ℝ) : A.dysonTermI B (n + 1) t = ∫ (s : ℝ) in 0..t, A.interactionPicture B s * A.dysonTermI B n s

★ The time-ordered recursion: dysonTermI (n + 1) t = ∫₀ᵗ V_I(s) · dysonTermI n s ds. Unrolled, dysonTermI n t = ∫_{0 ≤ s₁ ≤ ⋯ ≤ sₙ ≤ t} V_I(sₙ) ⋯ V_I(s₁) ds — the n vertices at ordered times, the latest on the left.

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

theorem Matrix.dysonTermI_one {m : Type u_1} [Fintype m] [DecidableEq m] (A B : Matrix m m ℂ) (t : ℝ) : A.dysonTermI B 1 t = ∫ (s : ℝ) in 0..t, A.interactionPicture B s

The one-vertex term: dysonTermI 1 t = ∫₀ᵗ V_I(s) ds.

The sum over vertex labellings

noncomputable def Matrix.dysonTermLabelled {m : Type u_1} [Fintype m] [DecidableEq m] (A : Matrix m m ℂ) {ι : Type u_2} (B : ι → Matrix m m ℂ) (n : ℕ) : (Fin n → ι) → ℝ → Matrix m m ℂ

The Dyson term with labelled vertices: the interaction B (f i) at the i-th slot, f 0 the latest vertex, Fin.tail f the earlier ones.

Equations

• A.dysonTermLabelled B 0 x_2 = fun (t : ℝ) => NormedSpace.exp (t • A)
• A.dysonTermLabelled B n.succ f = fun (t : ℝ) => NormedSpace.exp (t • A) * ∫ (s : ℝ) in 0..t, NormedSpace.exp (-s • A) * B (f 0) * A.dysonTermLabelled B n (Fin.tail f) s

theorem Matrix.dysonTermLabelled_zero {m : Type u_1} [Fintype m] [DecidableEq m] (A : Matrix m m ℂ) {ι : Type u_2} (B : ι → Matrix m m ℂ) (f : Fin 0 → ι) (t : ℝ) : A.dysonTermLabelled B 0 f t = NormedSpace.exp (t • A)

theorem Matrix.dysonTermLabelled_succ {m : Type u_1} [Fintype m] [DecidableEq m] (A : Matrix m m ℂ) {ι : Type u_2} (B : ι → Matrix m m ℂ) (n : ℕ) (f : Fin (n + 1) → ι) (t : ℝ) : A.dysonTermLabelled B (n + 1) f t = NormedSpace.exp (t • A) * ∫ (s : ℝ) in 0..t, NormedSpace.exp (-s • A) * B (f 0) * A.dysonTermLabelled B n (Fin.tail f) s

theorem Matrix.continuous_dysonTermLabelled {m : Type u_1} [Fintype m] [DecidableEq m] (A : Matrix m m ℂ) {ι : Type u_2} (B : ι → Matrix m m ℂ) (n : ℕ) (f : Fin n → ι) : Continuous (A.dysonTermLabelled B n f)

theorem Matrix.dysonTerm_sum_eq_sum_dysonTermLabelled {m : Type u_1} [Fintype m] [DecidableEq m] (A : Matrix m m ℂ) {ι : Type u_2} [Fintype ι] (B : ι → Matrix m m ℂ) (n : ℕ) (t : ℝ) : A.dysonTerm (∑ v : ι, B v) n t = ∑ f : Fin n → ι, A.dysonTermLabelled B n f t

★ The sum over vertex labellings. For an interaction that is a sum of vertex types, B = ∑ v, B v, the n-th Dyson term is the sum over every assignment f : Fin n → ι of a type to each of the n ordered vertices of the labelled term.

A diagonal free generator: old-fashioned perturbation theory

theorem Matrix.exp_smul_diagonal {m : Type u_1} [Fintype m] [DecidableEq m] (a : m → ℂ) (t : ℝ) : NormedSpace.exp (t • diagonal a) = diagonal fun (i : m) => Complex.exp (↑t * a i)

theorem Matrix.interactionPicture_diagonal_apply {m : Type u_1} [Fintype m] [DecidableEq m] (a : m → ℂ) (B : Matrix m m ℂ) (s : ℝ) (i j : m) : (diagonal a).interactionPicture B s i j = Complex.exp (↑s * (a j - a i)) * B i j

In the eigenbasis of the free generator the interaction-picture vertex is the bare vertex dressed with the free phases of its two legs: V_I(s) i j = e^{s (aⱼ − aᵢ)} · B i j.

theorem Matrix.dysonTermI_succ_apply_diagonal {m : Type u_1} [Fintype m] [DecidableEq m] (a : m → ℂ) (B : Matrix m m ℂ) (n : ℕ) (t : ℝ) (i j : m) : (diagonal a).dysonTermI B (n + 1) t i j = ∫ (s : ℝ) in 0..t, ∑ k : m, Complex.exp (↑s * (a k - a i)) * B i k * (diagonal a).dysonTermI B n s k j

★ Old-fashioned perturbation theory, one vertex at a time: in the eigenbasis of the free generator, dysonTermI (n + 1) t i j = ∫₀ᵗ ∑ₖ e^{s (aₖ − aᵢ)} B i k · dysonTermI n s k j ds — the sum over the intermediate state k between the latest vertex and the earlier ones.

theorem Matrix.dysonTermI_one_apply_diagonal {m : Type u_1} [Fintype m] [DecidableEq m] (a : m → ℂ) (B : Matrix m m ℂ) (t : ℝ) (i j : m) : (diagonal a).dysonTermI B 1 t i j = ∫ (s : ℝ) in 0..t, Complex.exp (↑s * (a j - a i)) * B i j

theorem Matrix.continuous_exp_mul_const (c : ℂ) : Continuous fun (s : ℝ) => Complex.exp (↑s * c)

theorem Matrix.dysonTerm_one_apply_diagonal_self {m : Type u_1} [Fintype m] [DecidableEq m] (a : m → ℂ) (B : Matrix m m ℂ) (t : ℝ) (i : m) : (diagonal a).dysonTerm B 1 t i i = Complex.exp (↑t * a i) * (↑t * B i i)

★ The first-order diagonal amplitude: D₁(t) i i = e^{t aᵢ} · t · B i i. The free phase of the state carries through and the vertex is inserted at every time s ∈ [0, t] with the same weight — with B a polynomial in the field and i the vacuum, the one-vertex vacuum diagram.

theorem Matrix.dysonTerm_one_apply_diagonal_of_ne {m : Type u_1} [Fintype m] [DecidableEq m] (a : m → ℂ) (B : Matrix m m ℂ) (t : ℝ) {i j : m} (h : a i ≠ a j) : (diagonal a).dysonTerm B 1 t i j = B i j * (Complex.exp (↑t * a j) - Complex.exp (↑t * a i)) / (a j - a i)

★ The first-order transition amplitude between distinct free levels: D₁(t) i j = B i j · (e^{t aⱼ} − e^{t aᵢ}) / (aⱼ − aᵢ) — for a = −i E the textbook ⟨j∣U(t)∣i⟩ ≈ −i V_{ji} (e^{−i E_j t} − e^{−i E_i t}) / (−i (E_j − E_i)) of time-dependent perturbation theory.

theorem Matrix.dysonTermI_two_apply_diagonal {m : Type u_1} [Fintype m] [DecidableEq m] (a : m → ℂ) (B : Matrix m m ℂ) (t : ℝ) (i j : m) : (diagonal a).dysonTermI B 2 t i j = ∫ (s₂ : ℝ) in 0..t, ∫ (s₁ : ℝ) in 0..s₂, ∑ k : m, Complex.exp (↑s₂ * (a k - a i)) * Complex.exp (↑s₁ * (a j - a k)) * (B i k * B k j)

★ The two-vertex amplitude: the double integral over the ordered times 0 ≤ s₁ ≤ s₂ ≤ t of the sum over the intermediate state k of the two vertex entries dressed with the free phases — the second-order term of old-fashioned perturbation theory.

theorem Matrix.dysonTermI_two_apply_diagonal_self {m : Type u_1} [Fintype m] [DecidableEq m] (a : m → ℂ) (B : Matrix m m ℂ) (t : ℝ) (i : m) : (diagonal a).dysonTermI B 2 t i i = ∫ (s₂ : ℝ) in 0..t, ∫ (s₁ : ℝ) in 0..s₂, ∑ k : m, Complex.exp ((↑s₂ - ↑s₁) * (a k - a i)) * (B i k * B k i)

The two-vertex amplitude on the diagonal: only the time difference s₂ − s₁ between the vertices enters the free propagation, e^{(s₂ − s₁) (aₖ − aᵢ)}.