The generator of a bounded perturbation: the mild solution is a classical one

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #129 (out of #64(iii)); consumed by SchrodingerGenerator.lean.

BoundedPerturbation.lean builds the perturbed semigroup 𝒮 = hS.perturbed B of a strongly continuous contraction semigroup S by a bounded B as the Dyson series, and characterises it by the Duhamel equation — a mild solution. This file proves the mild solution is classical on the generator's domain, without ever naming an unbounded operator: the generator is read off the orbit as a right derivative at time zero.

• HasGeneratorAt T ψ v: the orbit t ↦ T t ψ has right derivative v at 0 — ψ lies in the domain of the generator of T and the generator sends it to v (hasGeneratorAt_iff_hasDerivWithinAt).
• ★ tendsto_inv_smul_duhamelIntegral: the Duhamel integral ∫₀ᵗ S(t−s) B 𝒮(s) χ ds is t · Bχ + o(t) — the one analytic input, from joint continuity of the integrand at (0, 0).
• ★★ hasGeneratorAt_perturbed_iff: the generator of 𝒮 is A + B on the domain of A, and the domains agree: HasGeneratorAt 𝒮 χ (v + Bχ) ↔ HasGeneratorAt S χ v.
• For any semigroup-like family (T 0 = 1, the law for nonnegative times, strong continuity, a bound on [0, t]): HasGeneratorAt.tendsto_right (right derivative along the orbit), HasGeneratorAt.apply (the orbit stays in the generator's domain, with gen (T t ψ) = T t (gen ψ)), ★★ HasGeneratorAt.hasDerivAt (two-sided derivative at every t > 0: the left difference quotient is T (t − k) applied to the right quotient at 0, controlled by the bound and strong continuity).
• ★★★ hasDerivAt_perturbed: for ψ in the domain of the generator of S with value v, and t > 0, d/dt 𝒮(t)ψ = 𝒮(t)(v + Bψ); hasDerivWithinAt_perturbed_zero at t = 0; ★★ hasGeneratorAt_of_perturbed: 𝒮(t)ψ stays in the domain of the generator of S, with A(𝒮(t)ψ) = 𝒮(t)(A + B)ψ − B(𝒮(t)ψ), so the equation also reads d/dt 𝒮(t)ψ = A(𝒮(t)ψ) + B(𝒮(t)ψ) (★★★ perturbed_classical).

Honest scope

• The generator is a right derivative, not an operator. HasGeneratorAt is the standard definition of the infinitesimal generator applied one vector at a time; no LinearPMap is formed and no closedness is used. Consumers that have the generator as an operator (SchrodingerGenerator.lean) connect through the derivative statement they already have.
• Nonnegative times. S and 𝒮 are extended by the identity to t ≤ 0, so at t = 0 only the derivative within [0, ∞) is stated. For t > 0 the derivative is two-sided.
• Nothing is said about the converse domain question for a concrete S — that a vector whose orbit has a right derivative lies in a concretely described domain — which is a statement about that S, not about the perturbation.

References: K.-J. Engel, R. Nagel, One-Parameter Semigroups for Linear Evolution Equations, II.1 (generators, the orbit in the domain), III.1 (bounded perturbations); A. Pazy, Semigroups of Linear Operators, Thm 3.1.1; BoundedPerturbation.lean (dysonSum_eq_add_integral, perturbed_add, norm_perturbed_le); specs/BACKLOG.md #129, #64.

The generator as a right derivative at time zero

def HasGeneratorAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (T : ℝ → E →L[ℂ] E) (ψ v : E) : Prop

HasGeneratorAt T ψ v: the orbit t ↦ T t ψ has right derivative v at 0, i.e. ψ is in the domain of the generator of T and the generator sends ψ to v.

Equations

• HasGeneratorAt T ψ v = Filter.Tendsto (fun (h : ℝ) => h⁻¹ • ((T h) ψ - ψ)) (nhdsWithin 0 (Set.Ioi 0)) (nhds v)

theorem HasGeneratorAt.unique {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {T : ℝ → E →L[ℂ] E} {ψ v v' : E} (h : HasGeneratorAt T ψ v) (h' : HasGeneratorAt T ψ v') : v = v'

theorem Ici_zero_diff_zero : Set.Ici 0 \ {0} = Set.Ioi 0

theorem hasGeneratorAt_iff_hasDerivWithinAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {T : ℝ → E →L[ℂ] E} (h0 : T 0 = 1) (ψ v : E) : HasGeneratorAt T ψ v ↔ HasDerivWithinAt (fun (t : ℝ) => (T t) ψ) v (Set.Ici 0) 0

The generator statement is the derivative of the orbit within [0, ∞) at 0.

Semigroup-like families: the orbit stays in the domain and is differentiable

theorem HasGeneratorAt.tendsto_right {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {T : ℝ → E →L[ℂ] E} (hadd : ∀ (s t : ℝ), 0 ≤ s → 0 ≤ t → T (s + t) = T s * T t) {ψ v : E} (hv : HasGeneratorAt T ψ v) {t : ℝ} (ht : 0 ≤ t) : Filter.Tendsto (fun (h : ℝ) => h⁻¹ • ((T (t + h)) ψ - (T t) ψ)) (nhdsWithin 0 (Set.Ioi 0)) (nhds ((T t) v))

The right derivative along the orbit: d⁺/dt T t ψ = T t v.

theorem HasGeneratorAt.apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {T : ℝ → E →L[ℂ] E} (hadd : ∀ (s t : ℝ), 0 ≤ s → 0 ≤ t → T (s + t) = T s * T t) {ψ v : E} (hv : HasGeneratorAt T ψ v) {t : ℝ} (ht : 0 ≤ t) : HasGeneratorAt T ((T t) ψ) ((T t) v)

★ The orbit stays in the generator's domain, and the generator commutes with the semigroup along it: gen (T t ψ) = T t (gen ψ).

theorem HasGeneratorAt.hasDerivAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {T : ℝ → E →L[ℂ] E} (hadd : ∀ (s t : ℝ), 0 ≤ s → 0 ≤ t → T (s + t) = T s * T t) (hcont : ∀ (ψ : E), Continuous fun (t : ℝ) => (T t) ψ) {t : ℝ} (ht : 0 < t) {M : ℝ} (hM : ∀ (s : ℝ), 0 ≤ s → s ≤ t → ‖T s‖ ≤ M) {ψ v : E} (hv : HasGeneratorAt T ψ v) : HasDerivAt (fun (s : ℝ) => (T s) ψ) ((T t) v) t

★★ The orbit is differentiable at every positive time, with derivative T t (gen ψ). The right derivative is tendsto_right; the left difference quotient at t is T (t − k) applied to the right quotient at 0, which the bound on [0, t] and strong continuity control.

The Duhamel integral is t · Bχ + o(t)

theorem ContractionSemigroup.tendsto_inv_smul_duhamelIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) (hS : IsContractionSemigroup S) (χ : E) : Filter.Tendsto (fun (t : ℝ) => t⁻¹ • ∫ (s : ℝ) in 0..t, (S (t - s)) (B (dysonSum S B s χ))) (nhdsWithin 0 (Set.Ioi 0)) (nhds (B χ))

★ The Duhamel integral has right derivative Bχ at 0: t⁻¹ ∫₀ᵗ S(t−s) B 𝒮(s) χ ds → Bχ, by joint continuity of the integrand at (0, 0).

The generator of the perturbed semigroup

theorem ContractionSemigroup.hasGeneratorAt_perturbed_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) (hS : IsContractionSemigroup S) (χ v : E) : HasGeneratorAt (hS.perturbed B) χ (v + B χ) ↔ HasGeneratorAt S χ v

★★ The generator of 𝒮 is A + B on the domain of A, and the domains agree.

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 : ℝ) : 0 ≤ s → 0 ≤ t → hS.perturbed B (s + t) = hS.perturbed B s * hS.perturbed B t

The perturbed family satisfies the semigroup law in the order hadd wants.

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

The perturbed family is bounded by e^{‖B‖ t} on [0, t].

theorem ContractionSemigroup.hasDerivAt_perturbed {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) (hS : IsContractionSemigroup S) {ψ v : E} (hv : HasGeneratorAt S ψ v) {t : ℝ} (ht : 0 < t) : HasDerivAt (fun (s : ℝ) => (hS.perturbed B s) ψ) ((hS.perturbed B t) (v + B ψ)) t

★★★ The mild solution is classical: for ψ in the domain of the generator of S with value v, the perturbed orbit is differentiable at every t > 0 with d/dt 𝒮(t)ψ = 𝒮(t)(v + Bψ).

theorem ContractionSemigroup.hasDerivWithinAt_perturbed_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) (hS : IsContractionSemigroup S) {ψ v : E} (hv : HasGeneratorAt S ψ v) : HasDerivWithinAt (fun (s : ℝ) => (hS.perturbed B s) ψ) (v + B ψ) (Set.Ici 0) 0

The same at t = 0, within [0, ∞): the derivative is v + Bψ.

theorem ContractionSemigroup.hasGeneratorAt_perturbed_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) (hS : IsContractionSemigroup S) {ψ v : E} (hv : HasGeneratorAt S ψ v) {t : ℝ} (ht : 0 ≤ t) : HasGeneratorAt (hS.perturbed B) ((hS.perturbed B t) ψ) ((hS.perturbed B t) (v + B ψ))

The perturbed orbit stays in the generator's domain of 𝒮, with gen (𝒮(t)ψ) = 𝒮(t)(v + Bψ).

theorem ContractionSemigroup.hasGeneratorAt_of_perturbed {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) (hS : IsContractionSemigroup S) {ψ v : E} (hv : HasGeneratorAt S ψ v) {t : ℝ} (ht : 0 ≤ t) : HasGeneratorAt S ((hS.perturbed B t) ψ) ((hS.perturbed B t) (v + B ψ) - B ((hS.perturbed B t) ψ))

★★ The perturbed orbit stays in the domain of the generator of S, with A(𝒮(t)ψ) = 𝒮(t)(A + B)ψ − B(𝒮(t)ψ).

theorem ContractionSemigroup.perturbed_classical {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {S : ℝ → E →L[ℂ] E} (B : E →L[ℂ] E) (hS : IsContractionSemigroup S) {ψ v : E} (hv : HasGeneratorAt S ψ v) {t : ℝ} (ht : 0 < t) : ∃ (w : E), HasGeneratorAt S ((hS.perturbed B t) ψ) w ∧ HasDerivAt (fun (s : ℝ) => (hS.perturbed B s) ψ) (w + B ((hS.perturbed B t) ψ)) t

★★★ The classical equation in the generator's own terms: at every t > 0 the orbit is differentiable, its point lies in the domain of the generator of S with a named value w, and the derivative is w + B(𝒮(t)ψ) — i.e. d/dt 𝒮(t)ψ = (A + B)(𝒮(t)ψ).