Documentation

TauCeti.Analysis.Semigroups.Generation.HilleYosida.Generation

The Hille--Yosida generation theorem #

This file completes the Yosida construction for a densely defined operator A on a real Banach space. At growth exponent zero, the resolvent-power estimates

‖R(lambda, A) ^ n‖ ≤ M / lambda ^ n

produce the semigroup hilleYosidaLimitSemigroup. The compact-time convergence of its bounded approximations and the shared positive resolvent half-line identify the generator of that semigroup with A.

For a general growth exponent omega, hilleYosidaSemigroup applies the zero-exponent construction to A - omega I, then exponentially shifts the resulting semigroup back. The scalar-shift identities for partial linear maps and semigroup generators show that its generator is exactly A, while its growth bound becomes (omega, M). The final characterization combines this construction with density and the sharp generator-resolvent estimates for every C₀-semigroup.

This proves the Hille--Yosida milestone in Part A of the one-parameter-semigroups roadmap.

Main results #

References #

Generator identification at exponent zero #

source
@[simp]
theorem TauCeti.Semigroups.hilleYosidaLimitSemigroup_generator {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} {M : ℝ} (hM : 1 ≤ M) (hres : ∀ (lambda : ℝ), 0 < lambda → lambda ∈ A.resolventSet) (hpow : ∀ (n : ℕ), 1 ≤ n → ∀ (lambda : ℝ), 0 < lambda → ‖A.resolvent lambda ^ n‖ ≤ M / lambda ^ n) (hdense : Dense ↑A.domain) :
(hilleYosidaLimitSemigroup hM hres hpow hdense).generator = A

The exponent-zero Hille--Yosida limit semigroup has generator A.

The first resolvent-power estimate makes the Yosida approximations converge to A on its dense domain. All power estimates together bound their exponentials by M, and the compact-time limit theorems identify those exponentials with the orbits of hilleYosidaLimitSemigroup. Finally, 1 is a resolvent point of both A and the limit generator, so the inclusion obtained from the integrated Cauchy equation is an equality.

The general generation theorem #

source
noncomputable def TauCeti.Semigroups.hilleYosidaSemigroup {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} {M omega : ℝ} (hM : 1 ≤ M) (hres : ∀ (lambda : ℝ), omega < lambda → lambda ∈ A.resolventSet) (hpow : ∀ (n : ℕ), 1 ≤ n → ∀ (lambda : ℝ), omega < lambda → ‖A.resolvent lambda ^ n‖ ≤ M / (lambda - omega) ^ n) (hdense : Dense ↑A.domain) :
StronglyContinuousSemigroup X

The strongly continuous semigroup constructed by the general (M, omega) Hille--Yosida theorem. It is the exponential unshift of the exponent-zero limit semigroup for A - omega I.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.Semigroups.hilleYosidaSemigroup_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} {M omega : ℝ} (hM : 1 ≤ M) (hres : ∀ (lambda : ℝ), omega < lambda → lambda ∈ A.resolventSet) (hpow : ∀ (n : ℕ), 1 ≤ n → ∀ (lambda : ℝ), omega < lambda → ‖A.resolvent lambda ^ n‖ ≤ M / (lambda - omega) ^ n) (hdense : Dense ↑A.domain) (t : NNReal) (x : X) :
    ((hilleYosidaSemigroup hM hres hpow hdense) t) x = Real.exp (omega * ↑t) • yosidaLimit (LinearPMap.subScalar A omega) (↑t) x

    Evaluating the general Hille--Yosida semigroup gives the exponentially shifted exponent-zero Yosida limit.

    source
    @[simp]
    theorem TauCeti.Semigroups.hilleYosidaSemigroup_realOperator_apply_of_nonneg {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} {M omega : ℝ} (hM : 1 ≤ M) (hres : ∀ (lambda : ℝ), omega < lambda → lambda ∈ A.resolventSet) (hpow : ∀ (n : ℕ), 1 ≤ n → ∀ (lambda : ℝ), omega < lambda → ‖A.resolvent lambda ^ n‖ ≤ M / (lambda - omega) ^ n) (hdense : Dense ↑A.domain) {t : ℝ} (ht : 0 ≤ t) (x : X) :
    ((hilleYosidaSemigroup hM hres hpow hdense).realOperator t) x = Real.exp (omega * t) • yosidaLimit (LinearPMap.subScalar A omega) t x

    Real-time evaluation of the general Hille--Yosida semigroup at a nonnegative time.

    source
    theorem TauCeti.Semigroups.tendsto_hilleYosidaSemigroup {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} {M omega : ℝ} (hM : 1 ≤ M) (hres : ∀ (lambda : ℝ), omega < lambda → lambda ∈ A.resolventSet) (hpow : ∀ (n : ℕ), 1 ≤ n → ∀ (lambda : ℝ), omega < lambda → ‖A.resolvent lambda ^ n‖ ≤ M / (lambda - omega) ^ n) (hdense : Dense ↑A.domain) (t : NNReal) (x : X) :
    Filter.Tendsto (fun (lambda : ℝ) => Real.exp (omega * ↑t) • (NormedSpace.exp (↑t • yosidaApproximation (LinearPMap.subScalar A omega) lambda)) x) Filter.atTop (nhds (((hilleYosidaSemigroup hM hres hpow hdense) t) x))

    The shifted Yosida approximations converge pointwise to the general Hille--Yosida semigroup.

    source
    @[simp]
    theorem TauCeti.Semigroups.hilleYosidaSemigroup_generator {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} {M omega : ℝ} (hM : 1 ≤ M) (hres : ∀ (lambda : ℝ), omega < lambda → lambda ∈ A.resolventSet) (hpow : ∀ (n : ℕ), 1 ≤ n → ∀ (lambda : ℝ), omega < lambda → ‖A.resolvent lambda ^ n‖ ≤ M / (lambda - omega) ^ n) (hdense : Dense ↑A.domain) :
    (hilleYosidaSemigroup hM hres hpow hdense).generator = A

    The general Hille--Yosida semigroup has generator A.

    source
    theorem TauCeti.Semigroups.hasGrowthBound_hilleYosidaSemigroup {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} {M omega : ℝ} (hM : 1 ≤ M) (hres : ∀ (lambda : ℝ), omega < lambda → lambda ∈ A.resolventSet) (hpow : ∀ (n : ℕ), 1 ≤ n → ∀ (lambda : ℝ), omega < lambda → ‖A.resolvent lambda ^ n‖ ≤ M / (lambda - omega) ^ n) (hdense : Dense ↑A.domain) :
    (hilleYosidaSemigroup hM hres hpow hdense).HasGrowthBound omega M

    The general Hille--Yosida semigroup has the prescribed growth bound (omega, M).

    source
    theorem TauCeti.Semigroups.hilleYosida_generation {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} {M omega : ℝ} (hM : 1 ≤ M) (hres : ∀ (lambda : ℝ), omega < lambda → lambda ∈ A.resolventSet) (hpow : ∀ (n : ℕ), 1 ≤ n → ∀ (lambda : ℝ), omega < lambda → ‖A.resolvent lambda ^ n‖ ≤ M / (lambda - omega) ^ n) (hdense : Dense ↑A.domain) :
    ∃ (S : StronglyContinuousSemigroup X), S.generator = A ∧ S.HasGrowthBound omega M

    Hille--Yosida generation theorem. Let A be a densely defined operator on a real Banach space, let 1 ≤ M, and suppose that every real lambda > omega belongs to the resolvent set of A, with the power estimates

    ‖R(lambda, A) ^ n‖ ≤ M / (lambda - omega) ^ n for every n ≥ 1.

    Then A generates a strongly continuous semigroup with growth bound (omega, M). The produced semigroup is the exponential unshift of the exponent-zero Yosida limit for A - omega I.

    source
    theorem TauCeti.Semigroups.hilleYosida_generation_iff {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (A : X →ₗ.[ℝ] X) (M omega : ℝ) :
    (∃ (S : StronglyContinuousSemigroup X), S.generator = A ∧ S.HasGrowthBound omega M) ↔ 1 ≤ M ∧ Dense ↑A.domain ∧ (∀ (lambda : ℝ), omega < lambda → lambda ∈ A.resolventSet) ∧ ∀ (n : ℕ), 1 ≤ n → ∀ (lambda : ℝ), omega < lambda → ‖A.resolvent lambda ^ n‖ ≤ M / (lambda - omega) ^ n

    Hille--Yosida characterization. An unbounded operator is the generator of a strongly continuous semigroup with growth bound (omega, M) if and only if 1 ≤ M, its domain is dense, the half-line (omega, ∞) lies in its resolvent set, and its resolvent powers satisfy the sharp Hille--Yosida estimates.