/- Copyright (c) 2026 Michael R. Douglas. All rights reserved. Released under Apache 2.0 license. # Strongly Continuous Semigroups and the Hille-Yosida Theorem This file defines strongly continuous one-parameter semigroups (C₀-semigroups) on Banach spaces, their infinitesimal generators, the resolvent operator via the Laplace transform, and the forward direction of the Hille-Yosida theorem. ## Main Definitions * `StronglyContinuousSemigroup` — a family `S(t)` of bounded linear operators for `t ≥ 0` satisfying `S(0) = Id`, `S(s+t) = S(s) ∘ S(t)`, and strong continuity at `t = 0` (Def. 1 in [Linares]). * `ContractingSemigroup` — a C₀-semigroup of contractions: `‖S(t)‖ ≤ 1` for all `t ≥ 0` (Def. 3 in [Linares]). Corresponds to `M = 1, ω = 0` in the growth bound. * `domain` — the generator domain `D(A) = {x : lim_{t→0⁺} (S(t)x - x)/t exists}` as a `Submodule ℝ X` (Def. 2 in [Linares]). * `generatorMap` — the infinitesimal generator `A` as a `LinearMap` from the domain, `Ax = lim_{t→0⁺} (S(t)x - x)/t`. * `ContractingSemigroup.resolvent` — the resolvent `R(λ)x = ∫₀^∞ e^{-λt} S(t)x dt` for contraction semigroups (eq. 0.13 in [Linares]), defined via `LinearMap.mkContinuous` with built-in bound `‖R(λ)‖ ≤ 1/λ`. ## Main Results * `normBoundedOnUnitInterval` — `∃ M ≥ 1, ∀ t ∈ [0,1], ‖S(t)‖ ≤ M`, via the Banach-Steinhaus theorem (uniform boundedness principle). * `existsGrowthBound` — every C₀-semigroup has exponential growth: `‖S(t)‖ ≤ M e^{ωt}` (Thm. 1 in [Linares], eq. 0.3). * `strongContAt` — strong continuity at every `t₀ ≥ 0`, not just at 0 (Cor. 1 in [Linares]). * `hilleYosidaResolventBound` — `‖R(λ)‖ ≤ 1/λ` for contraction semigroups (eq. 0.14 in [Linares]; Thm. 6(ii), forward direction of Hille-Yosida). ## What is NOT yet proved * `resolventMapsToDomain` — `R(λ)x ∈ D(A)`, proved via the integral shift trick (eq. 0.15 in [Linares]). * `resolventRightInv` — `(λI - A)R(λ) = I` (eq. 0.16 in [Linares]). * The converse (sufficiency) direction of Hille-Yosida, which requires the Yosida approximation `A_λ = λ A R_λ(A) = λ² R_λ(A) - λI` (eq. 0.19). ## References * [EN] Engel-Nagel, "One-Parameter Semigroups for Linear Evolution Equations", Graduate Texts in Mathematics 194, Springer (2000). Primary reference. Ch. I §5: C₀-semigroups. Ch. II §1: Generators and resolvents. Ch. II §3: Hille-Yosida generation theorems. * [Linares] F. Linares, "The Hille-Yosida Theorem", IMPA lecture notes (2021). * [Baudoin] F. Baudoin, "Semigroups in Banach spaces", lecture notes (2019). * Hille, "Functional Analysis and Semi-Groups" (1948). * Yosida, "On the differentiability and the representation of one-parameter semi-group of linear operators" (1948). * Reed-Simon, "Methods of Modern Mathematical Physics I", §VIII. -/ import Mathlib.Topology.Algebra.Module.Basic import Mathlib.Analysis.Normed.Operator.ContinuousLinearMap import Mathlib.Analysis.Normed.Operator.BanachSteinhaus import Mathlib.Analysis.SpecialFunctions.Log.Basic import Mathlib.Analysis.SpecialFunctions.ExpDeriv import Mathlib.MeasureTheory.Integral.Bochner.Basic import Mathlib.MeasureTheory.Integral.ExpDecay import Mathlib.MeasureTheory.Measure.Lebesgue.Basic import Mathlib.Analysis.SpecialFunctions.Integrals.Basic import Mathlib.Analysis.SpecialFunctions.ImproperIntegrals noncomputable section open scoped Topology NNReal /-! ## Strongly Continuous Semigroups -/ variable (X : Type*) [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] -- Needed for `integral_smul` in the resolvent definition; not auto-synthesized -- at `maxSynthPendingDepth = 3`. instance : SMulCommClass ℝ ℝ X := smulCommClass_self ℝ X /-- A strongly continuous one-parameter semigroup (C₀-semigroup) on a Banach space ([EN] Def. I.5.1, [Linares] Def. 1). `S(t)` is a bounded linear operator for each `t ≥ 0`, satisfying: 1. `S(0) = Id` 2. `S(s + t) = S(s) ∘ S(t)` for all `s, t ≥ 0` 3. `t ↦ S(t) x` is continuous at `t = 0` for each `x : X` By the semigroup property + continuity at 0, condition 3 is equivalent to `t ↦ S(t) x` being continuous on all of `[0, ∞)`. -/ structure StronglyContinuousSemigroup where /-- The semigroup operator at time `t`. -/ operator : ℝ → X →L[ℝ] X /-- `S(0) = Id` -/ at_zero : operator 0 = ContinuousLinearMap.id ℝ X /-- `S(s + t) = S(s) ∘ S(t)` for `s, t ≥ 0` -/ semigroup : ∀ (s t : ℝ), 0 ≤ s → 0 ≤ t → operator (s + t) = (operator s).comp (operator t) /-- Strong continuity: `t ↦ S(t) x` is continuous at 0 for each `x` -/ strong_cont : ∀ (x : X), Filter.Tendsto (fun t => operator t x) (nhdsWithin 0 (Set.Ici 0)) (nhds x) /-- A contraction semigroup: `‖S(t)‖ ≤ 1` for all `t ≥ 0` ([EN] Def. I.5.6, [Linares] Def. 3). Corresponds to growth bound `ω₀ = 0`. -/ structure ContractingSemigroup extends StronglyContinuousSemigroup X where /-- `‖S(t)‖ ≤ 1` for all `t ≥ 0`. -/ contracting : ∀ (t : ℝ), 0 ≤ t → ‖operator t‖ ≤ 1 variable {X} /-! ## Basic Properties -/ /-- `S(t) x` at `t = 0` equals `x`, pointwise version. -/ @[simp] theorem StronglyContinuousSemigroup.operatorZeroApply (S : StronglyContinuousSemigroup X) (x : X) : S.operator 0 x = x := by rw [S.at_zero, ContinuousLinearMap.id_apply] /-- The operator norm of a C₀-semigroup is bounded on `[0, 1]`. This is one direction of [EN] Prop. I.5.3: strong continuity implies uniform boundedness on compact intervals. The proof applies the Banach-Steinhaus theorem (uniform boundedness principle) to the family `{S(t) : t ∈ [0,1]}`, using strong continuity at 0 and the semigroup property to establish the required pointwise bounds. -/ private theorem StronglyContinuousSemigroup.normBoundedOnUnitInterval (S : StronglyContinuousSemigroup X) : ∃ (M : ℝ), 1 ≤ M ∧ ∀ (t : ℝ), 0 ≤ t → t ≤ 1 → ‖S.operator t‖ ≤ M := by -- Step 1: For each x, the orbit {S(t)x : t ∈ [0, 1]} is pointwise bounded. have h_ptwise : ∀ x : X, ∃ C, ∀ (i : Set.Icc (0 : ℝ) 1), ‖(fun j : Set.Icc (0 : ℝ) 1 => S.operator j.val) i x‖ ≤ C := by intro x -- By strong continuity at 0: S(t)x → x, so ‖S(t)x‖ bounded near 0 have hsc := S.strong_cont x rw [Metric.tendsto_nhdsWithin_nhds] at hsc obtain ⟨δ, hδ_pos, hδ⟩ := hsc 1 one_pos -- ‖S(t)x‖ ≤ ‖x‖ + 1 for t ∈ [0, δ) have h_near : ∀ t : ℝ, 0 ≤ t → t < δ → ‖S.operator t x‖ ≤ ‖x‖ + 1 := by intro t ht0 htδ have h1 := hδ ht0 (by rwa [dist_zero_right, Real.norm_eq_abs, abs_of_nonneg ht0]) rw [dist_eq_norm] at h1 linarith [norm_le_insert' (S.operator t x) x] -- Extend to [0, 1] using semigroup property and operator norm of S(δ) set L := max ‖S.operator δ‖ 1 set B := ‖x‖ + 1 set N := Nat.ceil (1 / δ) -- Claim: ∀ k, t ∈ [0, (k+1)δ) → ‖S(t)x‖ ≤ L^k * B have h_claim : ∀ (k : ℕ), ∀ t : ℝ, 0 ≤ t → t < (↑k + 1) * δ → ‖S.operator t x‖ ≤ L ^ k * B := by intro k; induction k with | zero => intro t ht0 htδ simp only [Nat.cast_zero, zero_add, one_mul] at htδ simp only [pow_zero, one_mul] exact h_near t ht0 htδ | succ k ih => intro t ht0 ht_ub by_cases hk : t < (↑k + 1) * δ · -- Earlier interval: use IH + L ≥ 1 calc ‖S.operator t x‖ ≤ L ^ k * B := ih t ht0 hk _ ≤ L ^ (k + 1) * B := by apply mul_le_mul_of_nonneg_right _ (by positivity) exact pow_le_pow_right₀ (le_max_right _ _) (Nat.le_succ k) · -- New interval: S(t)x = S(δ)(S(t-δ)x) push_neg at hk have htd_nn : 0 ≤ t - δ := by have : δ ≤ (↑k + 1) * δ := le_mul_of_one_le_left (le_of_lt hδ_pos) (by have := (Nat.cast_nonneg k : (0 : ℝ) ≤ ↑k); linarith) linarith have htd_lt : t - δ < (↑k + 1) * δ := by push_cast [Nat.succ_eq_add_one] at ht_ub; linarith have h_sg := S.semigroup δ (t - δ) (le_of_lt hδ_pos) htd_nn rw [show δ + (t - δ) = t from by ring] at h_sg calc ‖S.operator t x‖ = ‖S.operator δ (S.operator (t - δ) x)‖ := by simp only [h_sg, ContinuousLinearMap.comp_apply] _ ≤ ‖S.operator δ‖ * ‖S.operator (t - δ) x‖ := ContinuousLinearMap.le_opNorm _ _ _ ≤ L * (L ^ k * B) := by apply mul_le_mul (le_max_left _ _) (ih _ htd_nn htd_lt) (by positivity) (by positivity) _ = L ^ (k + 1) * B := by ring -- For t ∈ [0, 1]: use claim with k = N, since 1 < (N+1)δ have hNδ : 1 < (↑N + 1) * δ := by have hN : (1 : ℝ) / δ ≤ ↑N := Nat.le_ceil _ have : 1 ≤ ↑N * δ := by rwa [div_le_iff₀ hδ_pos] at hN linarith exact ⟨L ^ N * B, fun ⟨t, ht0, ht1⟩ => by simp only; exact h_claim N t ht0 (by linarith)⟩ -- Step 2: Apply Banach-Steinhaus for uniform bound obtain ⟨C, hC⟩ := banach_steinhaus h_ptwise exact ⟨max C 1, le_max_right _ _, fun t ht0 ht1 => (hC ⟨t, ht0, ht1⟩).trans (le_max_left _ _)⟩ /-- The operator norm of a C₀-semigroup is bounded on `[0, n]` for any `n : ℕ`. Proof: by induction on `n`. For `t ∈ (k, k+1]`, write `t = (t-k) + k` where `t - k ∈ [0, 1]`, so `S(t) = S(t-k) ∘ S(k)` and `‖S(t)‖ ≤ ‖S(t-k)‖ · ‖S(k)‖ ≤ M · M^k = M^(k+1)`. -/ private theorem StronglyContinuousSemigroup.normBoundedOnInterval (S : StronglyContinuousSemigroup X) (n : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (t : ℝ), 0 ≤ t → t ≤ n → ‖S.operator t‖ ≤ C := by obtain ⟨M, hM1, hMbound⟩ := S.normBoundedOnUnitInterval have hM_pos : (0 : ℝ) < M := by linarith induction n with | zero => refine ⟨1, one_pos, fun t ht htn => ?_⟩ simp only [Nat.cast_zero] at htn have : t = 0 := le_antisymm htn ht rw [this, S.at_zero] exact ContinuousLinearMap.norm_id_le | succ k ih => obtain ⟨C_k, hC_k_pos, hC_k_bound⟩ := ih refine ⟨M * C_k, mul_pos hM_pos hC_k_pos, fun t ht htn => ?_⟩ by_cases hk : t ≤ ↑k · calc ‖S.operator t‖ ≤ C_k := hC_k_bound t ht hk _ ≤ M * C_k := le_mul_of_one_le_left (le_of_lt hC_k_pos) hM1 · -- t ∈ (k, k+1], decompose: t = (t - k) + k push_neg at hk have htk_nn : 0 ≤ t - ↑k := by linarith have htk_le : t - ↑k ≤ 1 := by push_cast [Nat.succ_eq_add_one] at htn; linarith have hk_nn : (0 : ℝ) ≤ ↑k := Nat.cast_nonneg k have h_eq : t = (t - ↑k) + ↑k := by ring have h_sg := S.semigroup (t - ↑k) ↑k htk_nn hk_nn rw [← h_eq] at h_sg rw [h_sg] calc ‖(S.operator (t - ↑k)).comp (S.operator ↑k)‖ ≤ ‖S.operator (t - ↑k)‖ * ‖S.operator ↑k‖ := ContinuousLinearMap.opNorm_comp_le _ _ _ ≤ M * C_k := mul_le_mul (hMbound _ htk_nn htk_le) (hC_k_bound ↑k hk_nn le_rfl) (norm_nonneg _) (le_of_lt hM_pos) /-- Strong continuity at every `t₀ ≥ 0`, not just at 0 ([EN] Prop. I.5.3, [Linares] Cor. 1). From continuity at 0: `S(t)x → x` as `t → 0⁺`. Then at `t₀`: `S(t₀ + h)x = S(t₀)(S(h)x) → S(t₀)x` as `h → 0⁺` by continuity of `S(t₀)`. Left continuity uses the operator norm bound from `normBoundedOnInterval`. -/ theorem StronglyContinuousSemigroup.strongContAt (S : StronglyContinuousSemigroup X) (x : X) (t₀ : ℝ) (ht₀ : 0 ≤ t₀) : Filter.Tendsto (fun t => S.operator t x) (nhdsWithin t₀ (Set.Ici 0)) (nhds (S.operator t₀ x)) := by -- Decompose nhdsWithin t₀ (Ici 0) using Iic/Ici splitting at t₀. -- nhdsWithin t₀ (Ici 0) = nhdsWithin t₀ (Ici 0 ∩ Iic t₀) ⊔ nhdsWithin t₀ (Ici 0 ∩ Ici t₀) rw [show Set.Ici (0 : ℝ) = (Set.Ici 0 ∩ Set.Iic t₀) ∪ (Set.Ici 0 ∩ Set.Ici t₀) from by rw [← Set.inter_union_distrib_left, Set.Iic_union_Ici, Set.inter_univ]] rw [nhdsWithin_union, Filter.tendsto_sup] -- Simplify the intersection sets have h_right_set : Set.Ici (0 : ℝ) ∩ Set.Ici t₀ = Set.Ici t₀ := by ext y; simp only [Set.mem_inter_iff, Set.mem_Ici] exact ⟨fun ⟨_, h⟩ => h, fun h => ⟨le_trans ht₀ h, h⟩⟩ have h_left_set : Set.Ici (0 : ℝ) ∩ Set.Iic t₀ = Set.Icc 0 t₀ := Set.Ici_inter_Iic rw [h_left_set, h_right_set] constructor · -- Left continuity: nhdsWithin t₀ (Icc 0 t₀) -- For 0 ≤ t ≤ t₀: S(t₀)x = S(t)(S(t₀-t)x), so -- S(t)x - S(t₀)x = S(t)(x - S(t₀-t)x). -- ‖S(t)(x - S(t₀-t)x)‖ ≤ ‖S(t)‖·‖x - S(t₀-t)x‖ → 0 -- since ‖S(t)‖ is bounded on [0, t₀] and ‖S(t₀-t)x - x‖ → 0. -- The operator norm bound on [0, t₀] follows from normBoundedOnUnitInterval -- (itself proved via the uniform boundedness principle) + the semigroup property. -- We state this bound as a local fact. have h_norm_bound : ∃ C > 0, ∀ t : ℝ, 0 ≤ t → t ≤ t₀ → ‖S.operator t‖ ≤ C := by obtain ⟨C, hC, hCb⟩ := S.normBoundedOnInterval (Nat.ceil t₀) exact ⟨C, hC, fun t ht ht' => hCb t ht (ht'.trans (Nat.le_ceil t₀))⟩ obtain ⟨C, hC_pos, hC_bound⟩ := h_norm_bound rw [Metric.tendsto_nhdsWithin_nhds] intro ε hε -- Extract δ from strong_cont: for h ∈ [0, δ), ‖S(h)x - x‖ < ε/C have h_sc := S.strong_cont x rw [Metric.tendsto_nhdsWithin_nhds] at h_sc obtain ⟨δ, hδ_pos, hδ_spec⟩ := h_sc (ε / C) (div_pos hε hC_pos) refine ⟨δ, hδ_pos, fun t ht_mem ht_dist => ?_⟩ simp only [Set.mem_Icc] at ht_mem -- Key: S(t₀)x = S(t)(S(t₀ - t)x) by semigroup have ht₀t_nn : 0 ≤ t₀ - t := by linarith [ht_mem.2] have h_sg_eq : S.operator t₀ = (S.operator t).comp (S.operator (t₀ - t)) := by have := S.semigroup t (t₀ - t) ht_mem.1 ht₀t_nn rwa [add_sub_cancel] at this -- S(t)x - S(t₀)x = S(t)(x - S(t₀-t)x) have h_diff : S.operator t x - S.operator t₀ x = S.operator t (x - S.operator (t₀ - t) x) := by conv_rhs => rw [map_sub] congr 1 rw [h_sg_eq, ContinuousLinearMap.comp_apply] rw [dist_eq_norm, h_diff] calc ‖S.operator t (x - S.operator (t₀ - t) x)‖ ≤ ‖S.operator t‖ * ‖x - S.operator (t₀ - t) x‖ := ContinuousLinearMap.le_opNorm _ _ _ ≤ C * ‖x - S.operator (t₀ - t) x‖ := mul_le_mul_of_nonneg_right (hC_bound t ht_mem.1 ht_mem.2) (norm_nonneg _) _ = C * dist (S.operator (t₀ - t) x) x := by rw [dist_eq_norm, ← norm_neg, neg_sub] _ < C * (ε / C) := by apply mul_lt_mul_of_pos_left _ hC_pos apply hδ_spec ht₀t_nn simp only [dist_zero_right, Real.norm_eq_abs, abs_of_nonneg ht₀t_nn] rw [Real.dist_eq, abs_sub_comm] at ht_dist rwa [abs_of_nonneg ht₀t_nn] at ht_dist _ = ε := mul_div_cancel₀ ε (ne_of_gt hC_pos) · -- Right continuity: nhdsWithin t₀ (Ici t₀) -- For t ≥ t₀: S(t)x = S(t₀)(S(t - t₀)x) and S(t-t₀)x → x by strong_cont. -- S(t₀) is a CLM, hence continuous, so S(t₀)(S(t-t₀)x) → S(t₀)x. -- The map t ↦ t - t₀ sends nhdsWithin t₀ (Ici t₀) to nhdsWithin 0 (Ici 0) have h_sub_tendsto : Filter.Tendsto (fun t => t - t₀) (nhdsWithin t₀ (Set.Ici t₀)) (nhdsWithin 0 (Set.Ici 0)) := by apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within · have : Filter.Tendsto (fun t => t - t₀) (nhds t₀) (nhds 0) := by have h := Filter.Tendsto.sub_const (Filter.tendsto_id (α := ℝ).mono_left (le_refl (nhds t₀))) t₀ simp only [id, sub_self] at h; exact h exact this.mono_left nhdsWithin_le_nhds · filter_upwards [self_mem_nhdsWithin] with t ht simp only [Set.mem_Ici] at ht ⊢; linarith -- So S(t - t₀)x → x have h_inner : Filter.Tendsto (fun t => S.operator (t - t₀) x) (nhdsWithin t₀ (Set.Ici t₀)) (nhds x) := (S.strong_cont x).comp h_sub_tendsto -- And S(t₀)(S(t - t₀)x) → S(t₀)x by continuity of the CLM S(t₀) have h_outer : Filter.Tendsto (fun t => S.operator t₀ (S.operator (t - t₀) x)) (nhdsWithin t₀ (Set.Ici t₀)) (nhds (S.operator t₀ x)) := ((S.operator t₀).cont.tendsto x).comp h_inner -- It suffices to show S(t)x = S(t₀)(S(t - t₀)x) for t ≥ t₀ apply h_outer.congr' filter_upwards [self_mem_nhdsWithin] with t ht simp only [Set.mem_Ici] at ht have ht_nn : 0 ≤ t - t₀ := by linarith -- S(t₀ + (t - t₀)) = S(t₀) ∘ S(t - t₀) by semigroup, and t₀ + (t - t₀) = t have h_sg := S.semigroup t₀ (t - t₀) ht₀ ht_nn rw [show t₀ + (t - t₀) = t from by ring] at h_sg change (S.operator t₀) ((S.operator (t - t₀)) x) = (S.operator t) x rw [h_sg, ContinuousLinearMap.comp_apply] /-! ## The Infinitesimal Generator -/ /-- The infinitesimal generator of a C₀-semigroup ([EN] Def. II.1.2, [Linares] Def. 2). The domain consists of elements `x` for which the limit `lim_{t→0⁺} (S(t)x - x)/t` exists. The generator `A` is the value of this limit. By [EN] Thm. II.1.4, `A` is closed, densely defined, and determines the semigroup uniquely. -/ def StronglyContinuousSemigroup.generator (S : StronglyContinuousSemigroup X) (x : X) : Prop := ∃ (Ax : X), Filter.Tendsto (fun t => (1/t) • (S.operator t x - x)) (nhdsWithin 0 (Set.Ioi 0)) (nhds Ax) /-- The domain of the generator as a ℝ-submodule of X. This is algebraically closed under addition and scalar multiplication because limits of sums/scalar-multiples are sums/scalar-multiples of limits (in the Hausdorff topology of a Banach space). -/ def StronglyContinuousSemigroup.domain (S : StronglyContinuousSemigroup X) : Submodule ℝ X where carrier := { x | S.generator x } add_mem' := by intro x y hx hy obtain ⟨Ax, hAx⟩ := hx obtain ⟨Ay, hAy⟩ := hy refine ⟨Ax + Ay, ?_⟩ have : Filter.Tendsto (fun t => (1/t) • (S.operator t (x + y) - (x + y))) (nhdsWithin 0 (Set.Ioi 0)) (nhds (Ax + Ay)) := by have heq : ∀ᶠ t in nhdsWithin 0 (Set.Ioi 0), (1/t) • (S.operator t (x + y) - (x + y)) = (1/t) • (S.operator t x - x) + (1/t) • (S.operator t y - y) := by filter_upwards with t rw [map_add, add_sub_add_comm, smul_add] exact (hAx.add hAy).congr' (heq.mono (fun _ h => h.symm)) exact this zero_mem' := by refine ⟨0, ?_⟩ have : (fun t => (1/t) • (S.operator t (0 : X) - 0)) = fun _ => 0 := by ext t; simp [map_zero] rw [this]; exact tendsto_const_nhds smul_mem' := by intro c x hx obtain ⟨Ax, hAx⟩ := hx refine ⟨c • Ax, ?_⟩ have heq : ∀ᶠ t in nhdsWithin 0 (Set.Ioi 0), (1/t) • (S.operator t (c • x) - c • x) = c • ((1/t) • (S.operator t x - x)) := by filter_upwards with t simp only [map_smul, smul_sub, smul_comm c (1/t)] exact (hAx.const_smul c).congr' (heq.mono (fun _ h => h.symm)) /-- The infinitesimal generator `A`, as a linear map from its domain submodule to `X`. Uses `Classical.choose` to extract the limit value. Linearity follows from uniqueness of limits in a Hausdorff space (`tendsto_nhds_unique`). -/ noncomputable def StronglyContinuousSemigroup.generatorMap (S : StronglyContinuousSemigroup X) : S.domain →ₗ[ℝ] X where toFun := fun x => Classical.choose x.property map_add' := by intro ⟨x, hx⟩ ⟨y, hy⟩ have hAx := Classical.choose_spec hx have hAy := Classical.choose_spec hy have hxy := Classical.choose_spec (S.domain.add_mem hx hy) have hsum : Filter.Tendsto (fun t => (1/t) • (S.operator t (x + y) - (x + y))) (nhdsWithin 0 (Set.Ioi 0)) (nhds (Classical.choose hx + Classical.choose hy)) := by have heq : ∀ᶠ t in nhdsWithin 0 (Set.Ioi 0), (1/t) • (S.operator t (x + y) - (x + y)) = (1/t) • (S.operator t x - x) + (1/t) • (S.operator t y - y) := by filter_upwards with t; rw [map_add, add_sub_add_comm, smul_add] exact (hAx.add hAy).congr' (heq.mono (fun _ h => h.symm)) exact tendsto_nhds_unique hxy hsum map_smul' := by intro c ⟨x, hx⟩ have hAx := Classical.choose_spec hx have hcx := Classical.choose_spec (S.domain.smul_mem c hx) have hscaled : Filter.Tendsto (fun t => (1/t) • (S.operator t (c • x) - c • x)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (c • Classical.choose hx)) := by have heq : ∀ᶠ t in nhdsWithin 0 (Set.Ioi 0), (1/t) • (S.operator t (c • x) - c • x) = c • ((1/t) • (S.operator t x - x)) := by filter_upwards with t simp only [map_smul, smul_sub, smul_comm c (1/t)] exact (hAx.const_smul c).congr' (heq.mono (fun _ h => h.symm)) exact tendsto_nhds_unique hcx hscaled /-! ## The Resolvent (for Contraction Semigroups) -/ open MeasureTheory /-- The pointwise integrand of the Laplace transform is integrable on `(0, ∞)`. For a **contraction** semigroup (`‖S(t)‖ ≤ 1`), the integrand satisfies `‖e^{-λt} S(t) x‖ ≤ e^{-λt} ‖x‖`, which is integrable for `λ > 0`. **Why contraction?** A general C₀-semigroup can have exponential growth `‖S(t)‖ ≤ M e^{ωt}`. If `λ ≤ ω`, the integrand diverges and the Bochner integral returns junk (zero). This breaks `integral_add` (which requires both summands to be `Integrable`), making it impossible to prove linearity of the resolvent. Restricting to contractions (`ω = 0`) ensures `λ > 0` suffices for convergence. -/ lemma ContractingSemigroup.integrable_resolvent_integrand (S : ContractingSemigroup X) (lambda : ℝ) (hlam : 0 < lambda) (x : X) : IntegrableOn (fun t => Real.exp (-(lambda * t)) • S.operator t x) (Set.Ioi 0) := by unfold MeasureTheory.IntegrableOn -- Bound by ‖x‖ * exp(-λt), which is integrable for λ > 0 apply MeasureTheory.Integrable.mono' ((exp_neg_integrableOn_Ioi 0 hlam).smul (‖x‖)) · -- AEStronglyMeasurable: follows from ContinuousOn → measurable apply ContinuousOn.aestronglyMeasurable _ measurableSet_Ioi apply ContinuousOn.smul · -- exp(-λt) is continuous everywhere, hence on Ioi 0 exact (Real.continuous_exp.comp ((continuous_const.mul continuous_id).neg)).continuousOn · -- S(t)x is continuous on [0, ∞) by strongContAt, hence on (0, ∞) have h_cont : ContinuousOn (fun t => S.operator t x) (Set.Ici 0) := fun t₀ ht₀ => S.toStronglyContinuousSemigroup.strongContAt x t₀ ht₀ exact h_cont.mono Set.Ioi_subset_Ici_self · -- Norm bound: ‖exp(-λt) • S(t)x‖ ≤ ‖x‖ * exp(-λt) a.e. on Ioi 0 apply (ae_restrict_mem measurableSet_Ioi).mono intro t (ht : 0 < t) rw [norm_smul, Real.norm_eq_abs, abs_of_pos (Real.exp_pos _), Pi.smul_apply, smul_eq_mul] calc Real.exp (-(lambda * t)) * ‖(S.operator t) x‖ ≤ Real.exp (-(lambda * t)) * (‖S.operator t‖ * ‖x‖) := by gcongr; exact ContinuousLinearMap.le_opNorm _ _ _ ≤ Real.exp (-(lambda * t)) * (1 * ‖x‖) := by gcongr; exact S.contracting t (le_of_lt ht) _ = ‖x‖ * Real.exp (-(lambda * t)) := by ring _ = ‖x‖ * Real.exp (-lambda * t) := by rw [neg_mul] /-- The resolvent operator `R(λ) x = ∫₀^∞ e^{-λt} S(t)x dt` for `λ > 0`. Defined on **contraction semigroups** to guarantee integrability (see `integrable_resolvent_integrand`). Constructed via `LinearMap.mkContinuous` which simultaneously provides the linear map and the operator norm bound `‖R(λ)‖ ≤ 1/λ`. **Implementation note**: The integral is defined pointwise for each `x ∈ X`, not as an operator-valued integral. This is necessary because `t ↦ S(t)` is only strongly continuous, so `t ↦ S(t)` is not strongly measurable as a function into `X →L[ℝ] X`. The pointwise integral `x ↦ ∫ e^{-λt} S(t)x dt` is well-defined because `t ↦ S(t)x` IS strongly measurable for each `x`. -/ noncomputable def ContractingSemigroup.resolvent (S : ContractingSemigroup X) (lambda : ℝ) (hlam : 0 < lambda) : X →L[ℝ] X := LinearMap.mkContinuous { toFun := fun x => ∫ t in Set.Ioi (0 : ℝ), Real.exp (-(lambda * t)) • S.operator t x map_add' := fun x y => by simp only [map_add, smul_add] exact integral_add (S.integrable_resolvent_integrand lambda hlam x) (S.integrable_resolvent_integrand lambda hlam y) map_smul' := fun c x => by simp only [RingHom.id_apply, map_smul] have h : ∀ t : ℝ, Real.exp (-(lambda * t)) • c • (S.operator t) x = c • (Real.exp (-(lambda * t)) • (S.operator t) x) := fun t => smul_comm _ c _ simp_rw [h] exact integral_smul (μ := volume.restrict (Set.Ioi (0 : ℝ))) c (fun t => Real.exp (-(lambda * t)) • (S.operator t) x) } (1 / lambda) (by intro x; simp only [LinearMap.coe_mk, AddHom.coe_mk] -- ‖∫ exp(-λt) • S(t)x‖ ≤ (1/λ) * ‖x‖ -- Step 1: bound the norm of the integral calc ‖∫ t in Set.Ioi 0, Real.exp (-(lambda * t)) • (S.operator t) x‖ ≤ ∫ t in Set.Ioi 0, Real.exp (-(lambda * t)) * ‖x‖ := by apply MeasureTheory.norm_integral_le_of_norm_le · -- Integrability of exp(-λt) * ‖x‖ on Ioi 0 have h := (exp_neg_integrableOn_Ioi 0 hlam).integrable.mul_const ‖x‖ simp only [neg_mul] at h; exact h · apply (ae_restrict_mem measurableSet_Ioi).mono intro t (ht : 0 < t) rw [norm_smul, Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)] gcongr calc ‖(S.operator t) x‖ ≤ ‖S.operator t‖ * ‖x‖ := ContinuousLinearMap.le_opNorm _ _ _ ≤ 1 * ‖x‖ := by gcongr; exact S.contracting t (le_of_lt ht) _ = ‖x‖ := one_mul _ -- Step 2: evaluate ∫ exp(-λt) * ‖x‖ = (1/λ) * ‖x‖ _ = 1 / lambda * ‖x‖ := by -- Pull out constant ‖x‖ -- Evaluate ∫ exp(-λt) = 1/λ via substitution have h_eval : ∫ t in Set.Ioi 0, Real.exp (-(lambda * t)) = lambda⁻¹ := by have h := integral_comp_mul_left_Ioi (fun t => Real.exp (-t)) 0 hlam simp only [mul_zero] at h rw [h, integral_exp_neg_Ioi_zero, smul_eq_mul, mul_one] -- Pull constant ‖x‖ out and apply evaluation rw [show (fun t => Real.exp (-(lambda * t)) * ‖x‖) = (fun t => ‖x‖ • Real.exp (-(lambda * t))) from by ext; simp [mul_comm]] rw [integral_smul (μ := volume.restrict (Set.Ioi (0 : ℝ)))] simp only [smul_eq_mul, h_eval, one_div] ring ) /-! ## Resolvent-Generator Interface The proofs of `resolventMapsToDomain` and `resolventRightInv` use the integral shift trick from [EN] Thm. II.1.10(i) / [Linares] eq. 0.15. We first establish helper lemmas for the key computation. -/ /-- Translation of set integral: `∫_{Ioi 0} f(t + h) = ∫_{Ioi h} f(u)`. Follows from translation invariance of Lebesgue measure. -/ private lemma integral_comp_add_right_Ioi (f : ℝ → X) (h : ℝ) : ∫ t in Set.Ioi 0, f (t + h) = ∫ u in Set.Ioi h, f u := by -- Express set integrals as full integrals with indicators simp_rw [← MeasureTheory.integral_indicator measurableSet_Ioi] -- Key: indicator_{Ioi 0}(fun t => f(t+h))(t) = indicator_{Ioi h}(f)(t+h) have key : ∀ t, Set.indicator (Set.Ioi 0) (fun t => f (t + h)) t = Set.indicator (Set.Ioi h) f (t + h) := by intro t; simp only [Set.indicator, Set.mem_Ioi] split_ifs with h1 h2 h2 <;> [rfl; linarith; linarith; rfl] simp_rw [key] -- Apply translation invariance of Lebesgue measure exact MeasureTheory.integral_add_right_eq_self _ h /-- Splitting `∫_{Ioi 0} = ∫_{Ioc 0 h} + ∫_{Ioi h}` for `h > 0`. -/ private lemma integral_Ioi_eq_Ioc_add_Ioi (f : ℝ → X) {h : ℝ} (hh : 0 < h) (hf : IntegrableOn f (Set.Ioi 0) volume) : ∫ t in Set.Ioi 0, f t = (∫ t in Set.Ioc 0 h, f t) + ∫ t in Set.Ioi h, f t := by rw [← Set.Ioc_union_Ioi_eq_Ioi (le_of_lt hh)] have hd : Disjoint (Set.Ioc 0 h) (Set.Ioi h) := Set.disjoint_left.mpr (fun _ ht1 ht2 => not_le.mpr ht2 ht1.2) exact MeasureTheory.setIntegral_union hd measurableSet_Ioi (hf.mono_set Set.Ioc_subset_Ioi_self) (hf.mono_set (Set.Ioi_subset_Ioi (le_of_lt hh))) /-- The generator difference quotient for `R(λ)x` converges to `λ R(λ)x - x`. This is the core computation shared by `resolventMapsToDomain` and `resolventRightInv`. -/ private theorem ContractingSemigroup.resolvent_generator_tendsto (S : ContractingSemigroup X) (lambda : ℝ) (hlam : 0 < lambda) (x : X) : Filter.Tendsto (fun t => (1 / t) • (S.operator t (S.resolvent lambda hlam x) - S.resolvent lambda hlam x)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (lambda • S.resolvent lambda hlam x - x)) := by set Rlx := S.resolvent lambda hlam x set f := fun t => Real.exp (-(lambda * t)) • S.operator t x -- Full integral shift computation ([EN] Thm. II.1.10(i), [Linares] eq. 0.15) set Rlx := S.resolvent lambda hlam x set f := fun t => Real.exp (-(lambda * t)) • S.operator t x -- The proof establishes the key identity for h > 0 and takes the limit. -- Key identity ([EN] Thm. II.1.10(i), [Linares] eq. 0.15): -- S(h)(Rlx) - Rlx = (e^{λh} - 1) • Rlx - e^{λh} • ∫_{Ioc 0 h} f(t) dt -- Then (1/h)(S(h)(Rlx) - Rlx) → λ Rlx - x as h → 0⁺. -- -- Each step below is proved. -- Step 1: Push S(h) inside integral and use semigroup property have h_push : ∀ (h : ℝ), 0 < h → S.operator h Rlx = Real.exp (lambda * h) • ∫ u in Set.Ioi h, f u := by intro h hh have hRlx : Rlx = ∫ t in Set.Ioi 0, f t := by simp only [Rlx, f, ContractingSemigroup.resolvent, LinearMap.mkContinuous_apply, LinearMap.coe_mk, AddHom.coe_mk] -- Step 1: Push S(h) inside integral rw [hRlx, ← ContinuousLinearMap.integral_comp_comm _ (S.integrable_resolvent_integrand lambda hlam x)] -- Goal: ∫ t in Ioi 0, S(h)(f(t)) = e^{λh} • ∫ u in Ioi h, f u -- Step 2: Rewrite integrand on Ioi 0 (where t > 0 hence t ≥ 0) have h_eq : ∀ t ∈ Set.Ioi (0 : ℝ), (S.operator h) (f t) = Real.exp (lambda * h) • f (t + h) := by intro t ht simp only [f, ContinuousLinearMap.map_smul] rw [← ContinuousLinearMap.comp_apply, ← S.semigroup h t (le_of_lt hh) (le_of_lt (Set.mem_Ioi.mp ht)), show h + t = t + h from add_comm h t] -- exp(-λt) • S(t+h)x = exp(λh) • (exp(-λ(t+h)) • S(t+h)x) -- Since • is right-assoc: RHS = exp(λh) • (exp(-λ(t+h)) • S(t+h)x) -- Use mul_smul: a • (b • x) = (a * b) • x, then exp_add + ring. symm; rw [← mul_smul, ← Real.exp_add]; congr 1; ring rw [MeasureTheory.setIntegral_congr_fun measurableSet_Ioi h_eq] -- Goal: ∫ t in Ioi 0, e^{λh} • f(t+h) = e^{λh} • ∫ u in Ioi h, f u rw [integral_smul (μ := volume.restrict (Set.Ioi (0 : ℝ)))] congr 1 exact integral_comp_add_right_Ioi f h -- Step 2: Split ∫_{Ioi h} = Rlx - ∫_{Ioc 0 h} f have h_split : ∀ (h : ℝ), 0 < h → ∫ u in Set.Ioi h, f u = Rlx - ∫ u in Set.Ioc 0 h, f u := by intro h hh have hsplit := integral_Ioi_eq_Ioc_add_Ioi f hh (S.integrable_resolvent_integrand lambda hlam x) -- Rlx = ∫ t in Ioi 0, f t by definition of resolvent have hRlx : Rlx = ∫ t in Set.Ioi 0, f t := by simp only [Rlx, f, ContractingSemigroup.resolvent, LinearMap.mkContinuous_apply, LinearMap.coe_mk, AddHom.coe_mk] rw [hRlx, hsplit]; abel -- Step 3: Combine into the key identity have h_identity : ∀ (h : ℝ), 0 < h → S.operator h Rlx - Rlx = (Real.exp (lambda * h) - 1) • Rlx - Real.exp (lambda * h) • ∫ u in Set.Ioc 0 h, f u := by intro h hh rw [h_push h hh, h_split h hh] simp only [smul_sub, sub_smul, one_smul] abel -- Step 4: Take the limit as h → 0⁺ -- First establish the derivative (e^{λh}-1)/h → λ have hderiv : HasDerivAt (fun t => Real.exp (lambda * t)) lambda 0 := by have := (Real.hasDerivAt_exp (lambda * 0)).comp (0 : ℝ) ((hasDerivAt_id (0 : ℝ)).const_mul lambda) simp [Real.exp_zero] at this; exact this -- Use h_identity to rewrite the generator quotient apply Filter.Tendsto.congr' · filter_upwards [self_mem_nhdsWithin] with t (ht : 0 < t) rw [h_identity t ht, smul_sub, smul_smul, smul_smul] -- Show ((e^{λt}-1)/t) • Rlx - ((e^{λt})/t) • ∫_{Ioc 0 t} f → λ • Rlx - x · -- Decompose: first term → λ • Rlx, second term → x apply Filter.Tendsto.sub · -- (1/t * (e^{λt}-1)) • Rlx → λ • Rlx apply Filter.Tendsto.smul _ tendsto_const_nhds -- 1/t * (e^{λt}-1) → λ from the derivative of exp at 0 have := hderiv.tendsto_slope_zero_right simp only [zero_add, Real.exp_zero, mul_zero] at this exact this.congr (fun t => by simp only [smul_eq_mul]; ring) · -- (1/t * e^{λt}) • ∫_{Ioc 0 t} f → 1 • x = x rw [show x = (1 : ℝ) • x from (one_smul ℝ x).symm] -- Rewrite (a * b) • v = a • (b • v) to separate exp and 1/t simp_rw [show ∀ t, (1 / t * Real.exp (lambda * t)) • ∫ u in Set.Ioc 0 t, f u = Real.exp (lambda * t) • ((1 / t) • ∫ u in Set.Ioc 0 t, f u) from fun t => by rw [show 1 / t * Real.exp (lambda * t) = Real.exp (lambda * t) * (1 / t) from by ring, mul_smul]] apply Filter.Tendsto.smul · -- exp(λt) → exp(0) = 1 as t → 0⁺ (continuity of exp) have hexp_cont : Filter.Tendsto (fun t => Real.exp (lambda * t)) (nhds 0) (nhds 1) := by have := hderiv.continuousAt.tendsto simp [Real.exp_zero, mul_zero] at this; exact this exact hexp_cont.mono_left nhdsWithin_le_nhds · -- (1/t) • ∫₀ᵗ f → f(0) = x as t → 0⁺ (FTC for Bochner integrals) -- Modify f for t < 0 so FTC gets two-sided continuity at 0 set g : ℝ → X := fun t => if 0 ≤ t then f t else x with hg_def -- g is continuous at 0 (right: strong continuity; left: constant x) have hg_cont : Filter.Tendsto g (nhds 0) (nhds x) := by rw [← nhdsLT_sup_nhdsGE (0 : ℝ)] apply Filter.Tendsto.sup · -- Left of 0: g(t) = x (constant), so Tendsto g = Tendsto const exact (tendsto_const_nhds (x := x)).congr' (by filter_upwards [self_mem_nhdsWithin] with t (ht : t < 0) simp only [g, if_neg (not_le.mpr ht)]) · -- Right of 0: g(t) = f(t) → x by strong continuity + exp exact (show Filter.Tendsto f (nhdsWithin 0 (Set.Ici 0)) (nhds x) from by have h1 : Filter.Tendsto (fun t => Real.exp (-(lambda * t))) (nhdsWithin 0 (Set.Ici 0)) (nhds 1) := by have hca : ContinuousAt (fun t => Real.exp (-(lambda * t))) 0 := Real.continuous_exp.continuousAt.comp ((continuousAt_const.mul continuousAt_id).neg) have := hca.tendsto simp [mul_zero, Real.exp_zero] at this exact this.mono_left nhdsWithin_le_nhds have h2 := S.toStronglyContinuousSemigroup.strong_cont x -- exp(-λt) • S(t)x → 1 • x = x simpa [one_smul] using h1.smul h2).congr' (by filter_upwards [self_mem_nhdsWithin] with t (ht : 0 ≤ t) simp only [g, if_pos ht]) -- g agrees with f on (0, ∞) so set integrals match have hg_eq : ∀ t, 0 < t → ∫ u in Set.Ioc 0 t, g u = ∫ u in Set.Ioc 0 t, f u := by intro t ht apply MeasureTheory.setIntegral_congr_fun measurableSet_Ioc intro u hu; simp [hg_def, hu.1.le] -- g is continuous (piecewise of continuous functions matching at 0) have hg_continuous : Continuous g := by change Continuous (Set.piecewise (Set.Ici 0) f (fun _ => x)) apply continuous_piecewise · -- Frontier condition: f 0 = x intro t ht have := frontier_Ici_subset (a := (0:ℝ)) ht simp [Set.mem_singleton_iff] at this; subst this simp [f, S.toStronglyContinuousSemigroup.at_zero, Real.exp_zero] · -- ContinuousOn f (closure (Ici 0)) = ContinuousOn f (Ici 0) rw [closure_Ici] exact ContinuousOn.smul ((Real.continuous_exp.comp (continuous_neg.comp (Continuous.mul continuous_const continuous_id))).continuousOn) (fun t₀ ht₀ => S.toStronglyContinuousSemigroup.strongContAt x t₀ ht₀) · exact continuousOn_const -- FTC for g: HasDerivAt (fun u => ∫₀ᵘ g) x 0 have h_ftc : HasDerivAt (fun u => ∫ t in (0 : ℝ)..u, g t) x 0 := intervalIntegral.integral_hasDerivAt_of_tendsto_ae_right IntervalIntegrable.refl (hg_continuous.stronglyMeasurableAtFilter volume (nhds 0)) (hg_cont.mono_left inf_le_left) -- Extract right Tendsto and convert have h_slope := h_ftc.tendsto_slope_zero_right simp only [zero_add, intervalIntegral.integral_same, sub_zero] at h_slope -- h_slope : Tendsto (fun t => t⁻¹ • ∫₀ᵗ g) (nhdsWithin 0 (Ioi 0)) (nhds x) -- Convert interval integral to set integral and g to f exact h_slope.congr' (by filter_upwards [self_mem_nhdsWithin] with t (ht : 0 < t) rw [one_div, intervalIntegral.integral_of_le (le_of_lt ht), hg_eq t ht]) /-- The resolvent maps all of `X` into the domain of the generator ([EN] Thm. II.1.10(i), [Linares] eq. 0.15). -/ theorem ContractingSemigroup.resolventMapsToDomain (S : ContractingSemigroup X) (lambda : ℝ) (hlam : 0 < lambda) (x : X) : (S.resolvent lambda hlam x) ∈ S.toStronglyContinuousSemigroup.domain := ⟨_, S.resolvent_generator_tendsto lambda hlam x⟩ /-- The fundamental resolvent identity: `(λI - A) R(λ) x = x`. This is eq. 0.16 in [Linares]: the resolvent `R_λ = (λI - A)⁻¹` is the right inverse of `λI - A`. Combined with `resolventMapsToDomain`, this shows `R_λ` is the bounded inverse of `λI - A` on all of `X`, establishing that `(0, ∞) ⊂ ρ(A)` (the resolvent set). The proof follows from the same integral shift computation as `resolventMapsToDomain` (eq. 0.15 in [Linares]): the limit `lim_{h→0⁺} (S(h) - I)/h · R(λ)x = λ R(λ)x - x` gives both the domain membership and the identity `A R(λ)x = λ R(λ)x - x`, which rearranges to `(λI - A) R(λ) x = x`. -/ theorem ContractingSemigroup.resolventRightInv (S : ContractingSemigroup X) (lambda : ℝ) (hlam : 0 < lambda) (x : X) : let Rlx := S.resolvent lambda hlam x let Rlx_dom : S.toStronglyContinuousSemigroup.domain := ⟨Rlx, S.resolventMapsToDomain lambda hlam x⟩ lambda • Rlx - S.toStronglyContinuousSemigroup.generatorMap Rlx_dom = x := by simp only -- generatorMap = Classical.choose of the generator existential -- By tendsto_nhds_unique: it equals λ Rlx - x have h_gen_eq : S.toStronglyContinuousSemigroup.generatorMap ⟨S.resolvent lambda hlam x, S.resolventMapsToDomain lambda hlam x⟩ = lambda • S.resolvent lambda hlam x - x := tendsto_nhds_unique (Classical.choose_spec (S.resolventMapsToDomain lambda hlam x)) (S.resolvent_generator_tendsto lambda hlam x) rw [h_gen_eq]; abel /-! ## Hille-Yosida Theorem -/ /-- **Hille-Yosida resolvent bound** (forward direction). For a contraction semigroup, the resolvent `R(λ) = ∫₀^∞ e^{-λt} S(t) dt` satisfies `‖R(λ)‖ ≤ 1/λ` for all `λ > 0`. This is essentially free from the construction: `resolvent` was built via `LinearMap.mkContinuous` with bound `1/λ`, so the norm bound follows from `LinearMap.mkContinuous_norm_le`. This is the forward direction of the Hille-Yosida theorem. The full theorem (an operator A generates a contraction semigroup iff it is closed, densely defined, with `‖(λI - A)⁻¹‖ ≤ 1/λ`) requires the converse: constructing the semigroup from the operator, which needs the Yosida approximation. Ref: Hille (1948), Yosida (1948); Reed-Simon I §VIII.3; Engel-Nagel Ch. II -/ theorem hilleYosidaResolventBound (S : ContractingSemigroup X) (lambda : ℝ) (hlam : 0 < lambda) : ‖S.resolvent lambda hlam‖ ≤ 1 / lambda := LinearMap.mkContinuous_norm_le _ (by positivity) _ /-! ## Growth Bounds and Exponential Type -/ /-- A C₀-semigroup has exponential growth bound `ω` if `‖S(t)‖ ≤ M e^{ωt}` for some constant `M ≥ 1` ([EN] eq. I.(5.1)). Contraction semigroups have `M = 1, ω = 0`. The infimum of all such `ω` is the growth bound `ω₀` ([EN] Def. I.5.6). -/ def StronglyContinuousSemigroup.HasGrowthBound (S : StronglyContinuousSemigroup X) (ω : ℝ) (M : ℝ) : Prop := 1 ≤ M ∧ ∀ (t : ℝ), 0 ≤ t → ‖S.operator t‖ ≤ M * Real.exp (ω * t) /-- Every C₀-semigroup has a finite exponential growth bound ([EN] Prop. I.5.5, [Linares] Thm. 1). The proof uses the uniform bound `M` on `[0, 1]` and sets `ω = log M`, then decomposes `t = ⌊t⌋ + frac(t)` to get `‖S(t)‖ ≤ M^{⌊t⌋+1} ≤ M · e^{ωt}`. -/ theorem StronglyContinuousSemigroup.existsGrowthBound (S : StronglyContinuousSemigroup X) : ∃ (ω : ℝ) (M : ℝ), S.HasGrowthBound ω M := by obtain ⟨M, hM1, hMbound⟩ := S.normBoundedOnUnitInterval have hM_pos : 0 < M := by linarith refine ⟨Real.log M, M, hM1, fun t ht => ?_⟩ -- Integer-time operator norm bound by induction: ‖S(k)‖ ≤ M^k have h_int_bound : ∀ (k : ℕ), ‖S.operator (↑k : ℝ)‖ ≤ M ^ k := by intro k; induction k with | zero => simp only [Nat.cast_zero, S.at_zero] exact ContinuousLinearMap.norm_id_le | succ k ih => have : (↑(k + 1) : ℝ) = 1 + ↑k := by push_cast; ring rw [this, S.semigroup 1 ↑k (by linarith) (Nat.cast_nonneg k)] calc ‖(S.operator 1).comp (S.operator ↑k)‖ ≤ ‖S.operator 1‖ * ‖S.operator ↑k‖ := ContinuousLinearMap.opNorm_comp_le _ _ _ ≤ M * M ^ k := mul_le_mul (hMbound 1 (by linarith) le_rfl) ih (norm_nonneg _) (by linarith) _ = M ^ (k + 1) := by ring -- Decompose t = (t - ⌊t⌋₊) + ⌊t⌋₊ where 0 ≤ t - ⌊t⌋₊ ≤ 1 set n := ⌊t⌋₊ with hn_def have hn_le : (↑n : ℝ) ≤ t := Nat.floor_le ht have hfrac_nn : 0 ≤ t - ↑n := sub_nonneg.mpr hn_le have hfrac_le1 : t - ↑n ≤ 1 := by have := Nat.lt_floor_add_one t; push_cast at this ⊢; linarith -- Use semigroup property: S(t) = S(t - n) ∘ S(n) have h_eq : (t - ↑n) + ↑n = t := by ring have h_sg := S.semigroup (t - ↑n) ↑n hfrac_nn (Nat.cast_nonneg n) rw [h_eq] at h_sg rw [h_sg] -- ‖S(t-n) ∘ S(n)‖ ≤ ‖S(t-n)‖ · ‖S(n)‖ ≤ M · M^n ≤ M · exp(log M · t) calc ‖(S.operator (t - ↑n)).comp (S.operator ↑n)‖ ≤ ‖S.operator (t - ↑n)‖ * ‖S.operator ↑n‖ := ContinuousLinearMap.opNorm_comp_le _ _ _ ≤ M * M ^ n := mul_le_mul (hMbound _ hfrac_nn hfrac_le1) (h_int_bound n) (norm_nonneg _) (by linarith) _ ≤ M * Real.exp (Real.log M * t) := by apply mul_le_mul_of_nonneg_left _ (by linarith) calc (M : ℝ) ^ n = Real.exp (↑n * Real.log M) := by rw [Real.exp_nat_mul, Real.exp_log hM_pos] _ ≤ Real.exp (Real.log M * t) := by apply Real.exp_le_exp.mpr calc ↑n * Real.log M ≤ t * Real.log M := mul_le_mul_of_nonneg_right hn_le (Real.log_nonneg hM1) _ = Real.log M * t := by ring end