A bounded perturbation of a strongly continuous contraction semigroup

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

Let S be a strongly continuous contraction semigroup on a Banach space E (IsContractionSemigroup: S (s + t) = S s * S t, ‖S t‖ ≤ 1, t ↦ S t ψ continuous; extended by the identity to negative times so that every integrand below is globally continuous), and B : E →L[ℂ] E bounded. No generator is named: the semigroup is the object. The Dyson series

D₀(t) ψ = S t ψ, Dₙ₊₁(t) ψ = ∫₀ᵗ S (t − s) (B (Dₙ(s) ψ)) ds

converges to the perturbed semigroup 𝒮(t) ψ = ∑ₙ Dₙ(t) ψ, the unique solution of the Duhamel (Volterra) equation 𝒮(t) ψ = S t ψ + ∫₀ᵗ S (t − s) (B (𝒮(s) ψ)) ds, and the Trotter product formula holds: (S (t/n) · exp ((t/n) B))ⁿ ψ → 𝒮(t) ψ.

This is Analysis/Matrix/DysonSeries.lean with exp (t A) replaced by a semigroup and the matrix Bochner integrals by vector-valued ones. It is the engine of the continuum path integral (Feynman–Kac and Nelson's theorem, specs/feynman-continuum-scoping.md FC-1): for the heat semigroup and B = −V the perturbed semigroup is e^{−t(H₀ + V)} without ever writing H₀.

• IsContractionSemigroup S — the predicate; continuous_uncurry — strong continuity plus the uniform bound give joint continuity of (t, ψ) ↦ S t ψ;
• dysonTerm S B n t ψ — the terms; continuous_dysonTerm (in t); dysonTerm_add, dysonTerm_smul (linear in ψ); ★ norm_dysonTerm_le — ‖Dₙ(t) ψ‖ ≤ (‖B‖ t)ⁿ / n! · ‖ψ‖;
• summable_dysonTerm, dysonSum S B t ψ = ∑' n, Dₙ(t) ψ, ★ norm_dysonSum_le — ‖𝒮(t) ψ‖ ≤ e^{‖B‖ t} ‖ψ‖, continuous_dysonSum;
• ★ dysonSum_eq_add_integral — the Duhamel equation; ★ eq_dysonSum_of_duhamel — its uniqueness: a continuous solution on [0, T] is the Dyson sum (the iterated Volterra bound M (‖B‖ t)ⁿ / n! → 0); ★★ dysonSum_add_time — the semigroup law 𝒮(t + s) = 𝒮(t) 𝒮(s), by uniqueness;
• IsContractionSemigroup.perturbed hS B t : E →L[ℂ] E — the bundled perturbed semigroup, with perturbed_apply, norm_perturbed_le, perturbed_zero, ★★ perturbed_add;
• trotterStep S B h = S h * exp (h • B); ★ norm_trotterStep_apply_sub_dysonSum_le — the one-step defect ‖(S h · e^{hB}) χ − 𝒮(h) χ‖ ≤ 2 (‖B‖ h)² e^{‖B‖ h} ‖χ‖ + h ω with ω the oscillation of S h (B χ) − S (h − s) (B (S s χ)) on [0, h]; exists_delta_of_isCompact — that oscillation is uniformly small on a compact set; pow_apply_sub_eq_sum — telescoping; ★★ tendsto_trotterStep_pow_apply — the Trotter product formula, (S (t/n) · exp ((t/n) B))ⁿ ψ → 𝒮(t) ψ, by telescoping against the semigroup law along the compact orbit {𝒮(s) ψ : s ∈ [0, t]};
• IsContractionSemigroup.of_group — a strongly continuous contraction group restricted to t ≥ 0 is a contraction semigroup: the real-time (unitary) case.

Three ways to the same operator. 𝒮(t) is the sum of the Dyson series, the unique solution of the Duhamel equation, and the Trotter limit of time-sliced products; the module proves all three agree. This is what lets the continuum path integral be compared across approaches: whatever construction satisfies the Duhamel equation is 𝒮.

Honest scope

⚠️ The semigroup is the primitive. Nothing here asserts that S is generated by an operator, or that 𝒮 is generated by A + B; at the pin there are no unbounded generators. 𝒮 is defined by the series and characterised by the Duhamel equation, which is what identifies it with any other construction of "e^{t(A+B)}".

References: F. J. Dyson, Phys. Rev. 75, 486 (1949); H. F. Trotter, Proc. AMS 10, 545 (1959); K.-J. Engel, R. Nagel, One-Parameter Semigroups for Linear Evolution Equations, III.1 (bounded perturbations) and III.5 (product formulas); Analysis/Matrix/DysonSeries.lean; Analysis/NormedSpace/TrotterGeneral.lean; specs/feynman-continuum-scoping.md; specs/BACKLOG.md #36(c).

Strongly continuous contraction semigroups

structure IsContractionSemigroup {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (S : ℝ → E →L[ℂ] E) : Prop

A strongly continuous contraction semigroup on E, extended by the identity to negative times: S (s + t) = S s * S t for s, t ≥ 0, ‖S t‖ ≤ 1, and t ↦ S t ψ continuous.

• eq_one_of_nonpos (t : ℝ) : t ≤ 0 → S t = 1
• map_add (s t : ℝ) : 0 ≤ s → 0 ≤ t → S (s + t) = S s * S t
• norm_le_one (t : ℝ) : ‖S t‖ ≤ 1
• continuous_apply (ψ : E) : Continuous fun (t : ℝ) => (S t) ψ

theorem IsContractionSemigroup.map_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {S : ℝ → E →L[ℂ] E} (hS : IsContractionSemigroup S) : S 0 = 1

theorem IsContractionSemigroup.norm_apply_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {S : ℝ → E →L[ℂ] E} (hS : IsContractionSemigroup S) (t : ℝ) (ψ : E) : ‖(S t) ψ‖ ≤ ‖ψ‖

theorem IsContractionSemigroup.continuous_uncurry {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {S : ℝ → E →L[ℂ] E} (hS : IsContractionSemigroup S) : Continuous fun (p : ℝ × E) => (S p.1) p.2

Strong continuity and the uniform bound give joint continuity of (t, ψ) ↦ S t ψ.

theorem IsContractionSemigroup.of_group {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (U : ℝ → E →L[ℂ] E) (h0 : U 0 = 1) (hadd : ∀ (s t : ℝ), U (s + t) = U s * U t) (hnorm : ∀ (t : ℝ), ‖U t‖ ≤ 1) (hcont : ∀ (ψ : E), Continuous fun (t : ℝ) => (U t) ψ) : IsContractionSemigroup fun (t : ℝ) => if 0 ≤ t then U t else 1

A strongly continuous one-parameter group of contractions (a unitary group, say), restricted to t ≥ 0 and extended by the identity, is a contraction semigroup: the real-time case of everything below.

The Dyson series

noncomputable def ContractionSemigroup.dysonTerm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (S : ℝ → E →L[ℂ] E) (B : E →L[ℂ] E) : ℕ → ℝ → E → E

The Dyson terms: D₀(t) ψ = S t ψ, Dₙ₊₁(t) ψ = ∫₀ᵗ S (t − s) (B (Dₙ(s) ψ)) ds.

Equations

• ContractionSemigroup.dysonTerm S B 0 = fun (t : ℝ) (ψ : E) => (S t) ψ
• ContractionSemigroup.dysonTerm S B n.succ = fun (t : ℝ) (ψ : E) => ∫ (s : ℝ) in 0..t, (S (t - s)) (B (ContractionSemigroup.dysonTerm S B n s ψ))

theorem ContractionSemigroup.dysonTerm_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (S : ℝ → E →L[ℂ] E) (B : E →L[ℂ] E) (t : ℝ) (ψ : E) : dysonTerm S B 0 t ψ = (S t) ψ

theorem ContractionSemigroup.dysonTerm_succ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (S : ℝ → E →L[ℂ] E) (B : E →L[ℂ] E) (n : ℕ) (t : ℝ) (ψ : E) : dysonTerm S B (n + 1) t ψ = ∫ (s : ℝ) in 0..t, (S (t - s)) (B (dysonTerm S B n s ψ))

theorem ContractionSemigroup.continuous_dysonTerm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) (hS : IsContractionSemigroup S) (n : ℕ) (ψ : E) : Continuous fun (t : ℝ) => dysonTerm S B n t ψ

theorem ContractionSemigroup.continuous_dysonTerm_integrand {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) (hS : IsContractionSemigroup S) (n : ℕ) (t : ℝ) (ψ : E) : Continuous fun (s : ℝ) => (S (t - s)) (B (dysonTerm S B n s ψ))

theorem ContractionSemigroup.dysonTerm_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) (hS : IsContractionSemigroup S) (n : ℕ) (t : ℝ) (ψ χ : E) : dysonTerm S B n t (ψ + χ) = dysonTerm S B n t ψ + dysonTerm S B n t χ

theorem ContractionSemigroup.dysonTerm_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) (n : ℕ) (t : ℝ) (c : ℂ) (ψ : E) : dysonTerm S B n t (c • ψ) = c • dysonTerm S B n t ψ

theorem ContractionSemigroup.norm_dysonTerm_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) (hS : IsContractionSemigroup S) (n : ℕ) {t : ℝ} (ht : 0 ≤ t) (ψ : E) : ‖dysonTerm S B n t ψ‖ ≤ (‖B‖ * t) ^ n / ↑n.factorial * ‖ψ‖

★ ‖Dₙ(t) ψ‖ ≤ (‖B‖ t)ⁿ / n! · ‖ψ‖ for 0 ≤ t.

theorem ContractionSemigroup.summable_norm_dysonTerm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) (hS : IsContractionSemigroup S) {t : ℝ} (ht : 0 ≤ t) (ψ : E) : Summable fun (n : ℕ) => ‖dysonTerm S B n t ψ‖

theorem ContractionSemigroup.summable_dysonTerm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) (hS : IsContractionSemigroup S) {t : ℝ} (ht : 0 ≤ t) (ψ : E) : Summable fun (n : ℕ) => dysonTerm S B n t ψ

noncomputable def ContractionSemigroup.dysonSum {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (S : ℝ → E →L[ℂ] E) (B : E →L[ℂ] E) (t : ℝ) (ψ : E) : E

The Dyson sum 𝒮(t) ψ = ∑' n, Dₙ(t) ψ, at time max t 0 (the identity for t ≤ 0).

Equations

• ContractionSemigroup.dysonSum S B t ψ = ∑' (n : ℕ), ContractionSemigroup.dysonTerm S B n (max t 0) ψ

theorem ContractionSemigroup.dysonSum_of_nonneg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) {t : ℝ} (ht : 0 ≤ t) (ψ : E) : dysonSum S B t ψ = ∑' (n : ℕ), dysonTerm S B n t ψ

theorem ContractionSemigroup.hasSum_dysonTerm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) (hS : IsContractionSemigroup S) {t : ℝ} (ht : 0 ≤ t) (ψ : E) : HasSum (fun (n : ℕ) => dysonTerm S B n t ψ) (dysonSum S B t ψ)

theorem ContractionSemigroup.norm_dysonSum_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) (hS : IsContractionSemigroup S) {t : ℝ} (ht : 0 ≤ t) (ψ : E) : ‖dysonSum S B t ψ‖ ≤ Real.exp (‖B‖ * t) * ‖ψ‖

★ ‖𝒮(t) ψ‖ ≤ e^{‖B‖ t} ‖ψ‖ for 0 ≤ t.

theorem ContractionSemigroup.dysonSum_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) (hS : IsContractionSemigroup S) (t : ℝ) (ψ χ : E) : dysonSum S B t (ψ + χ) = dysonSum S B t ψ + dysonSum S B t χ

theorem ContractionSemigroup.dysonSum_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) (t : ℝ) (c : ℂ) (ψ : E) : dysonSum S B t (c • ψ) = c • dysonSum S B t ψ

theorem ContractionSemigroup.dysonSum_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) (hS : IsContractionSemigroup S) (ψ : E) : dysonSum S B 0 ψ = ψ

theorem ContractionSemigroup.continuousOn_dysonSum_Iic {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) (hS : IsContractionSemigroup S) (ψ : E) (T : ℝ) : ContinuousOn (fun (t : ℝ) => dysonSum S B t ψ) (Set.Iic T)

The Dyson sum is continuous in time, by uniform convergence of the series on [0, T].

theorem ContractionSemigroup.continuous_dysonSum {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) (hS : IsContractionSemigroup S) (ψ : E) : Continuous fun (t : ℝ) => dysonSum S B t ψ

The Duhamel equation

theorem ContractionSemigroup.continuous_dysonSum_integrand {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) (hS : IsContractionSemigroup S) (t : ℝ) (ψ : E) : Continuous fun (s : ℝ) => (S (t - s)) (B (dysonSum S B s ψ))

The integrand of the Duhamel equation is continuous.

theorem ContractionSemigroup.dysonSum_eq_add_integral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) (hS : IsContractionSemigroup S) {t : ℝ} (ht : 0 ≤ t) (ψ : E) : dysonSum S B t ψ = (S t) ψ + ∫ (s : ℝ) in 0..t, (S (t - s)) (B (dysonSum S B s ψ))

★ The Duhamel equation: 𝒮(t) ψ = S t ψ + ∫₀ᵗ S (t − s) (B (𝒮(s) ψ)) ds for 0 ≤ t.

theorem ContractionSemigroup.integral_norm_pow_div_factorial {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (B : E →L[ℂ] E) (n : ℕ) (t : ℝ) : ∫ (s : ℝ) in 0..t, ‖B‖ * ((‖B‖ * s) ^ n / ↑n.factorial) = (‖B‖ * t) ^ (n + 1) / ↑(n + 1).factorial

The Volterra integral of the bound (‖B‖ s)ⁿ / n! is the next term of the exponential series.

theorem ContractionSemigroup.eq_dysonSum_of_duhamel {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) (hS : IsContractionSemigroup S) {T : ℝ} {X : ℝ → E} (hX : ContinuousOn X (Set.Icc 0 T)) (ψ : E) (hX' : ∀ t ∈ Set.Icc 0 T, X t = (S t) ψ + ∫ (s : ℝ) in 0..t, (S (t - s)) (B (X s))) (t : ℝ) : t ∈ Set.Icc 0 T → X t = dysonSum S B t ψ

★ Uniqueness for the Duhamel equation. A continuous solution of X t = S t ψ + ∫₀ᵗ S (t − s) (B (X s)) ds on [0, T] is the Dyson sum.

theorem ContractionSemigroup.dysonSum_add_time {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) (hS : IsContractionSemigroup S) {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (ψ : E) : dysonSum S B (t + s) ψ = dysonSum S B t (dysonSum S B s ψ)

★★ The semigroup law: 𝒮(t + s) ψ = 𝒮(t) (𝒮(s) ψ) for s, t ≥ 0, by uniqueness for the Duhamel equation.

The perturbed semigroup as an operator

theorem ContractionSemigroup.dysonSum_max {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) (t : ℝ) (ψ : E) : dysonSum S B (max t 0) ψ = dysonSum S B t ψ

noncomputable def IsContractionSemigroup.perturbed {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {S : ℝ → E →L[ℂ] E} (hS : IsContractionSemigroup S) (B : E →L[ℂ] E) (t : ℝ) : E →L[ℂ] E

★ The perturbed semigroup 𝒮(t) as a continuous linear map, ‖𝒮(t)‖ ≤ e^{‖B‖ t}.

Equations

• hS.perturbed B t = { toFun := ContractionSemigroup.dysonSum S B t, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous (Real.exp (‖B‖ * max t 0)) ⋯

theorem ContractionSemigroup.perturbed_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) (hS : IsContractionSemigroup S) (t : ℝ) (ψ : E) : (hS.perturbed B t) ψ = dysonSum S B t ψ

theorem ContractionSemigroup.norm_perturbed_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) (hS : IsContractionSemigroup S) (t : ℝ) : ‖hS.perturbed B t‖ ≤ Real.exp (‖B‖ * max t 0)

theorem ContractionSemigroup.perturbed_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) (hS : IsContractionSemigroup S) : hS.perturbed B 0 = 1

theorem ContractionSemigroup.perturbed_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) (hS : IsContractionSemigroup S) {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) : hS.perturbed B (t + s) = hS.perturbed B t * hS.perturbed B s

★★ The perturbed semigroup is a semigroup: 𝒮(t + s) = 𝒮(t) * 𝒮(s) for s, t ≥ 0.

theorem ContractionSemigroup.continuous_perturbed_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) (hS : IsContractionSemigroup S) (ψ : E) : Continuous fun (t : ℝ) => (hS.perturbed B t) ψ

The Trotter product formula

noncomputable def ContractionSemigroup.trotterStep {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (S : ℝ → E →L[ℂ] E) (B : E →L[ℂ] E) (h : ℝ) : E →L[ℂ] E

The Trotter step S h · exp (h B).

Equations

• ContractionSemigroup.trotterStep S B h = S h * NormedSpace.exp (h • B)

theorem ContractionSemigroup.trotterStep_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) (h : ℝ) (χ : E) : (trotterStep S B h) χ = (S h) ((NormedSpace.exp (h • B)) χ)

theorem ContractionSemigroup.norm_trotterStep_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) [Nontrivial E] (hS : IsContractionSemigroup S) {h : ℝ} (hh : 0 ≤ h) : ‖trotterStep S B h‖ ≤ Real.exp (h * ‖B‖)

theorem ContractionSemigroup.norm_trotterStep_pow_apply_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) [Nontrivial E] (hS : IsContractionSemigroup S) {h : ℝ} (hh : 0 ≤ h) (m : ℕ) (χ : E) : ‖(trotterStep S B h ^ m) χ‖ ≤ Real.exp (↑m * h * ‖B‖) * ‖χ‖

theorem ContractionSemigroup.pow_apply_sub_eq_sum {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (F : E →L[ℂ] E) (u : ℕ → E) (n : ℕ) : (F ^ n) (u 0) - u n = ∑ k ∈ Finset.range n, (F ^ (n - 1 - k)) (F (u k) - u (k + 1))

Telescoping a product against a sequence: Fⁿ (u 0) − u n = ∑ₖ F^{n−1−k} (F (u k) − u (k+1)).

theorem ContractionSemigroup.tsum_pow_div_factorial_add_two_le {x : ℝ} (hx : 0 ≤ x) : ∑' (n : ℕ), x ^ (n + 2) / ↑(n + 2).factorial ≤ x ^ 2 * Real.exp x

The tail of the exponential series: ∑ₙ xⁿ⁺²/(n+2)! ≤ x² eˣ for 0 ≤ x.

theorem ContractionSemigroup.norm_dysonSum_sub_sub_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) (hS : IsContractionSemigroup S) {h : ℝ} (hh : 0 ≤ h) (χ : E) : ‖dysonSum S B h χ - (S h) χ - dysonTerm S B 1 h χ‖ ≤ (‖B‖ * h) ^ 2 * Real.exp (‖B‖ * h) * ‖χ‖

The Dyson series beyond first order: ‖𝒮(h) χ − S h χ − D₁(h) χ‖ ≤ (‖B‖ h)² e^{‖B‖ h} ‖χ‖.

theorem ContractionSemigroup.trotterStep_apply_sub_dysonSum {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) (hS : IsContractionSemigroup S) (h : ℝ) (χ : E) : (trotterStep S B h) χ - dysonSum S B h χ = ((S h) ((NormedSpace.exp (h • B)) χ - χ - h • B χ) + ∫ (s : ℝ) in 0..h, (S h) (B χ) - (S (h - s)) (B ((S s) χ))) - (dysonSum S B h χ - (S h) χ - dysonTerm S B 1 h χ)

The one-step defect, decomposed: the second-order remainder of exp (h B), the integral of S h (B χ) − S (h − s) (B (S s χ)) over [0, h], and the Dyson tail.

theorem ContractionSemigroup.norm_trotterStep_apply_sub_dysonSum_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) (hS : IsContractionSemigroup S) {h : ℝ} (hh : 0 ≤ h) (χ : E) {ω : ℝ} (hω : ∀ s ∈ Set.Icc 0 h, ‖(S h) (B χ) - (S (h - s)) (B ((S s) χ))‖ ≤ ω) : ‖(trotterStep S B h) χ - dysonSum S B h χ‖ ≤ 2 * ((‖B‖ * h) ^ 2 * Real.exp (‖B‖ * h) * ‖χ‖) + h * ω

★ The one-step defect bound: if ‖S h (B χ) − S (h − s) (B (S s χ))‖ ≤ ω on [0, h], then ‖(S h · exp (h B)) χ − 𝒮(h) χ‖ ≤ 2 (‖B‖ h)² e^{‖B‖ h} ‖χ‖ + h ω.

theorem ContractionSemigroup.exists_delta_of_isCompact {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) (hS : IsContractionSemigroup S) {K : Set E} (hK : IsCompact K) {ε : ℝ} (hε : 0 < ε) : ∃ δ > 0, ∀ h ∈ Set.Icc 0 δ, ∀ s ∈ Set.Icc 0 h, ∀ χ ∈ K, ‖(S h) (B χ) - (S (h - s)) (B ((S s) χ))‖ ≤ ε

Uniformity on a compact set: for every ε > 0 there is δ > 0 with ‖S h (B χ) − S (h − s) (B (S s χ))‖ ≤ ε for all 0 ≤ s ≤ h ≤ δ and all χ in a compact K.

theorem ContractionSemigroup.norm_trotterStep_pow_apply_sub_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) [Nontrivial E] (hS : IsContractionSemigroup S) {t : ℝ} (ht : 0 ≤ t) (ψ : E) {n : ℕ} (hn : 0 < n) {ε₁ : ℝ} (hε₁ : ∀ k ∈ Finset.range n, ∀ s ∈ Set.Icc 0 (t / ↑n), ‖(S (t / ↑n)) (B (dysonSum S B (↑k * (t / ↑n)) ψ)) - (S (t / ↑n - s)) (B ((S s) (dysonSum S B (↑k * (t / ↑n)) ψ)))‖ ≤ ε₁) : ‖(trotterStep S B (t / ↑n) ^ n) ψ - dysonSum S B t ψ‖ ≤ Real.exp (t * ‖B‖) * (↑n * (2 * ((‖B‖ * (t / ↑n)) ^ 2 * Real.exp (‖B‖ * (t / ↑n)) * (Real.exp (‖B‖ * t) * ‖ψ‖)) + t / ↑n * ε₁))

The telescoped bound for the n-step product, given a uniform bound ε₁ on the one-step defect integrand along the orbit 𝒮(k t/n) ψ.

theorem ContractionSemigroup.tendsto_trotterStep_pow_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) [Nontrivial E] (hS : IsContractionSemigroup S) {t : ℝ} (ht : 0 ≤ t) (ψ : E) : Filter.Tendsto (fun (n : ℕ) => (trotterStep S B (t / ↑n) ^ n) ψ) Filter.atTop (nhds (dysonSum S B t ψ))

★★ The Trotter product formula for a bounded perturbation of a strongly continuous contraction semigroup: (S (t/n) · exp ((t/n) B))ⁿ ψ → 𝒮(t) ψ for every ψ and 0 ≤ t.