Semigroups

Results named in Tau Ceti's TauCeti.Analysis.Semigroups modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremThe bounded perturbation theorem#

If a strongly continuous semigroup S has growth bound (omega, M) and B is bounded, then B +ᵥ S.generator generates a strongly continuous semigroup with growth bound (omega + M * ‖B‖, M).

TauCeti.Semigroups.StronglyContinuousSemigroup.exists_generator_eq_vadd.{u_1} {X : Type u_1}
  [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X]
  (S : TauCeti.Semigroups.StronglyContinuousSemigroup X) {omega M : ℝ}
  (hb : S.HasGrowthBound omega M) (B : X →L[ℝ] X) :
  ∃ T, T.generator = ↑B +ᵥ S.generator ∧ T.HasGrowthBound (omega + M * ‖B‖) M

Lean

Formalized in Tau Ceti as TauCeti.Semigroups.StronglyContinuousSemigroup.exists_generator_eq_vadd.

Other forms

The bounded perturbation theorem. Formalized in Tau Ceti as TauCeti.Semigroups.StronglyContinuousSemigroup.exists_generator_eq_vadd_of_hasGrowthBound_one.

TauCeti.Semigroups.StronglyContinuousSemigroup.exists_generator_eq_vadd_of_hasGrowthBound_one.{u_1}
  {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X]
  (S : TauCeti.Semigroups.StronglyContinuousSemigroup X) {omega : ℝ} (hb : S.HasGrowthBound omega 1)
  (B : X →L[ℝ] X) : ∃ T, T.generator = ↑B +ᵥ S.generator ∧ T.HasGrowthBound (omega + ‖B‖) 1

The bounded perturbation theorem for contraction semigroups. Formalized in Tau Ceti as TauCeti.Semigroups.ContractionSemigroup.exists_generator_eq_vadd.

TauCeti.Semigroups.ContractionSemigroup.exists_generator_eq_vadd.{u_1} {X : Type u_1}
  [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X]
  (S : TauCeti.Semigroups.ContractionSemigroup X) (B : X →L[ℝ] X) :
  ∃ T, T.generator = ↑B +ᵥ S.generator ∧ T.HasGrowthBound ‖B‖ 1

The bounded perturbation theorem, operator form. Formalized in Tau Ceti as TauCeti.Semigroups.IsMDissipative.exists_stronglyContinuousSemigroup_generator_eq_vadd.

TauCeti.Semigroups.IsMDissipative.exists_stronglyContinuousSemigroup_generator_eq_vadd.{u_1}
  {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {A : X →ₗ.[ℝ] X} [CompleteSpace X]
  (hA : TauCeti.Semigroups.IsMDissipative A) (hdense : Dense ↑A.domain) (B : X →L[ℝ] X) :
  ∃ S, S.generator = ↑B +ᵥ A ∧ S.HasGrowthBound ‖B‖ 1

Sources

• Tau Ceti documentation: TauCeti.Semigroups.StronglyContinuousSemigroup.exists_generator_eq_vadd
• Source of TauCeti.Semigroups.StronglyContinuousSemigroup.exists_generator_eq_vadd in TauCeti/Analysis/Semigroups/Generation/BoundedPerturbation.lean

LeanTauCeti.Semigroups.StronglyContinuousSemigroup.exists_generator_eq_vadd · TauCeti.Semigroups.StronglyContinuousSemigroup.exists_generator_eq_vadd_of_hasGrowthBound_one · TauCeti.Semigroups.ContractionSemigroup.exists_generator_eq_vadd · TauCeti.Semigroups.IsMDissipative.exists_stronglyContinuousSemigroup_generator_eq_vadd

Uses 2

Proof usesConverse of the Lumer--Phillips theorem · Lumer--Phillips in duality-map form

TheoremConverse of the Lumer--Phillips theorem#

the generator of a contraction semigroup is dissipative.

It is the (ω, M) = (0, 1) case of the resolvent-range inequality StronglyContinuousSemigroup.norm_le_norm_smul_sub_generator. Together with StronglyContinuousSemigroup.smul_sub_generator_surjective and the density of the generator domain, it shows that the hypotheses of the Lumer--Phillips generation theorem are also necessary.

TauCeti.Semigroups.ContractionSemigroup.isDissipative_generator.{u_1} {X : Type u_1}
  [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X]
  (S : TauCeti.Semigroups.ContractionSemigroup X) : TauCeti.Semigroups.IsDissipative S.generator

Lean

Formalized in Tau Ceti as TauCeti.Semigroups.ContractionSemigroup.isDissipative_generator.

Other forms

The converse of the Lumer--Phillips theorem on a Hilbert space. Formalized in Tau Ceti as TauCeti.Semigroups.ContractionSemigroup.real_inner_generator_nonpos.

TauCeti.Semigroups.ContractionSemigroup.real_inner_generator_nonpos.{u_1} {X : Type u_1}
  [NormedAddCommGroup X] [InnerProductSpace ℝ X] [CompleteSpace X]
  (S : TauCeti.Semigroups.ContractionSemigroup X) (x : ↥S.generator.domain) :
  inner ℝ (↑S.generator x) ↑x ≤ 0

Sources

• Tau Ceti documentation: TauCeti.Semigroups.ContractionSemigroup.isDissipative_generator
• Source of TauCeti.Semigroups.ContractionSemigroup.isDissipative_generator in TauCeti/Analysis/Semigroups/Dissipative/Basic.lean

LeanTauCeti.Semigroups.ContractionSemigroup.isDissipative_generator · TauCeti.Semigroups.ContractionSemigroup.real_inner_generator_nonpos

Uses 1 · Used by 2

Proof usesHille–Yosida resolvent bound

Used byLumer--Phillips in duality-map form · The bounded perturbation theorem

TheoremThe Hille--Yosida bound at a complex spectral parameter#

on the half-plane of a growth bound (omega, M), ‖R(lambda, A)‖ ≤ M / (re lambda - omega).

TauCeti.Semigroups.StronglyContinuousSemigroup.norm_resolvent_complexGenerator_le.{u_1}
  {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] [CompleteSpace X] {omega M : ℝ}
  {lambda : ℂ} (S : TauCeti.Semigroups.StronglyContinuousSemigroup X) (hS : S.IsComplexLinear)
  (hb : S.HasGrowthBound omega M) (hlambda : omega < lambda.re) :
  ‖(S.complexGenerator hS).resolvent lambda‖ ≤ M / (lambda.re - omega)

Lean

Formalized in Tau Ceti as TauCeti.Semigroups.StronglyContinuousSemigroup.norm_resolvent_complexGenerator_le.

Sources

• Tau Ceti documentation: TauCeti.Semigroups.StronglyContinuousSemigroup.norm_resolvent_complexGenerator_le
• Source of TauCeti.Semigroups.StronglyContinuousSemigroup.norm_resolvent_complexGenerator_le in TauCeti/Analysis/Semigroups/Resolvent/Complex.lean

LeanTauCeti.Semigroups.StronglyContinuousSemigroup.norm_resolvent_complexGenerator_le

Uses 1

Proof usesHille–Yosida resolvent bound

TheoremThe Hille--Yosida power bounds at a complex spectral parameter#

on the half-plane of a growth bound (omega, M), ‖R(lambda, A)ⁿ‖ ≤ M / (re lambda - omega)ⁿ for every n.

TauCeti.Semigroups.StronglyContinuousSemigroup.norm_resolvent_complexGenerator_pow_le.{u_1}
  {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] [CompleteSpace X] {omega M : ℝ}
  {lambda : ℂ} (S : TauCeti.Semigroups.StronglyContinuousSemigroup X) (hS : S.IsComplexLinear)
  (hb : S.HasGrowthBound omega M) (hlambda : omega < lambda.re) (n : ℕ) :
  ‖(S.complexGenerator hS).resolvent lambda ^ n‖ ≤ M / (lambda.re - omega) ^ n

Lean

Formalized in Tau Ceti as TauCeti.Semigroups.StronglyContinuousSemigroup.norm_resolvent_complexGenerator_pow_le.

Sources

• Tau Ceti documentation: TauCeti.Semigroups.StronglyContinuousSemigroup.norm_resolvent_complexGenerator_pow_le
• Source of TauCeti.Semigroups.StronglyContinuousSemigroup.norm_resolvent_complexGenerator_pow_le in TauCeti/Analysis/Semigroups/Resolvent/Complex.lean

LeanTauCeti.Semigroups.StronglyContinuousSemigroup.norm_resolvent_complexGenerator_pow_le

Uses 1

Proof usesHille–Yosida resolvent bound

TheoremHille–Yosida resolvent bound#

‖R λ‖ ≤ M/(λ-ω) for a C₀ semigroup with growth bound (ω, M) and λ > ω (Hille 1948, Yosida 1948; Engel–Nagel Ch. II).

TauCeti.Semigroups.StronglyContinuousSemigroup.resolvent_norm_le.{u_1} {X : Type u_1}
  [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X]
  (S : TauCeti.Semigroups.StronglyContinuousSemigroup X) {ω M : ℝ} (hb : S.HasGrowthBound ω M)
  (lambda : ℝ) (hlam : ω < lambda) : ‖S.resolvent hb lambda hlam‖ ≤ M / (lambda - ω)

Lean

Formalized in Tau Ceti as TauCeti.Semigroups.StronglyContinuousSemigroup.resolvent_norm_le.

Other forms

Hille--Yosida resolvent bound for the resolvent of the generator. Formalized in Tau Ceti as TauCeti.Semigroups.StronglyContinuousSemigroup.norm_generator_resolvent_le.

TauCeti.Semigroups.StronglyContinuousSemigroup.norm_generator_resolvent_le.{u_1} {X : Type u_1}
  [NormedAddCommGroup X] [NormedSpace ℝ X] (S : TauCeti.Semigroups.StronglyContinuousSemigroup X)
  [CompleteSpace X] {omega M : ℝ} (hb : S.HasGrowthBound omega M) {lambda : ℝ}
  (hlambda : omega < lambda) : ‖S.generator.resolvent lambda‖ ≤ M / (lambda - omega)

Sources

• Tau Ceti documentation: TauCeti.Semigroups.StronglyContinuousSemigroup.resolvent_norm_le
• Source of TauCeti.Semigroups.StronglyContinuousSemigroup.resolvent_norm_le in TauCeti/Analysis/Semigroups/Resolvent/Basic.lean

LeanTauCeti.Semigroups.StronglyContinuousSemigroup.resolvent_norm_le · TauCeti.Semigroups.StronglyContinuousSemigroup.norm_generator_resolvent_le

Used by 4

Used byConverse of the Lumer--Phillips theorem · Sharp Hille--Yosida power bound for the generator resolvent · The Hille--Yosida bound at a complex spectral parameter · The Hille--Yosida power bounds at a complex spectral parameter

TheoremLumer--Phillips in duality-map form#

An unbounded operator on a real Banach space generates a contraction semigroup exactly when it is densely defined, each x ∈ D(A) has a duality-set member f with f (A x) ≤ 0, and lambda • I - A maps D(A) onto X for some lambda > 0.

TauCeti.Semigroups.exists_contractionSemigroup_generator_eq_iff_exists_mem_dualitySet_apply_nonpos.{u_1}
  {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (A : X →ₗ.[ℝ] X) :
  (∃ S, S.generator = A) ↔
    Dense ↑A.domain ∧
      (∀ (x : ↥A.domain), ∃ f ∈ TauCeti.dualitySet ℝ ↑x, f (↑A x) ≤ 0) ∧
        ∃ lambda, 0 < lambda ∧ Function.Surjective fun x => lambda • ↑x - ↑A x

Lean

Formalized in Tau Ceti as TauCeti.Semigroups.exists_contractionSemigroup_generator_eq_iff_exists_mem_dualitySet_apply_nonpos.

Other forms

Lumer--Phillips as a characterization. Formalized in Tau Ceti as TauCeti.Semigroups.exists_contractionSemigroup_generator_eq_iff.

TauCeti.Semigroups.exists_contractionSemigroup_generator_eq_iff.{u_1} {X : Type u_1}
  [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (A : X →ₗ.[ℝ] X) :
  (∃ S, S.generator = A) ↔ Dense ↑A.domain ∧ TauCeti.Semigroups.IsMDissipative A

The Lumer--Phillips generation theorem. Formalized in Tau Ceti as TauCeti.Semigroups.IsMDissipative.exists_contractionSemigroup_generator_eq.

TauCeti.Semigroups.IsMDissipative.exists_contractionSemigroup_generator_eq.{u_1} {X : Type u_1}
  [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X}
  (hA : TauCeti.Semigroups.IsMDissipative A) (hdense : Dense ↑A.domain) : ∃ S, S.generator = A

Lumer--Phillips with the universal duality-set sign condition. Formalized in Tau Ceti as TauCeti.Semigroups.exists_contractionSemigroup_generator_eq_iff_forall_mem_dualitySet_apply_nonpos.

TauCeti.Semigroups.exists_contractionSemigroup_generator_eq_iff_forall_mem_dualitySet_apply_nonpos.{u_1}
  {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (A : X →ₗ.[ℝ] X) :
  (∃ S, S.generator = A) ↔
    Dense ↑A.domain ∧
      (∀ (x : ↥A.domain), ∀ f ∈ TauCeti.dualitySet ℝ ↑x, f (↑A x) ≤ 0) ∧
        ∃ lambda, 0 < lambda ∧ Function.Surjective fun x => lambda • ↑x - ↑A x

Sources

• Tau Ceti documentation: TauCeti.Semigroups.exists_contractionSemigroup_generator_eq_iff_exists_mem_dualitySet_apply_nonpos
• Source of TauCeti.Semigroups.exists_contractionSemigroup_generator_eq_iff_exists_mem_dualitySet_apply_nonpos in TauCeti/Analysis/Semigroups/Generation/LumerPhillips.lean

LeanTauCeti.Semigroups.exists_contractionSemigroup_generator_eq_iff_exists_mem_dualitySet_apply_nonpos · TauCeti.Semigroups.exists_contractionSemigroup_generator_eq_iff · TauCeti.Semigroups.IsMDissipative.exists_contractionSemigroup_generator_eq · TauCeti.Semigroups.exists_contractionSemigroup_generator_eq_iff_forall_mem_dualitySet_apply_nonpos

Uses 2 · Used by 3

Proof usesConverse of the Lumer--Phillips theorem · The Duhamel identity for the exponential of a bounded operator

Used byHille--Yosida for contraction semigroups · Stone's theorem · The bounded perturbation theorem

TheoremSharp Hille--Yosida power bound for the generator resolvent#

For a C₀-semigroup with growth bound (omega, M) and lambda > omega, ‖R(lambda, generator S) ^ n‖ ≤ M / (lambda - omega) ^ n.

This is the necessity estimate in exactly the form consumed by the Hille--Yosida generation theorem.

TauCeti.Semigroups.StronglyContinuousSemigroup.norm_generator_resolvent_pow_le.{u_1} {X : Type u_1}
  [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X]
  (S : TauCeti.Semigroups.StronglyContinuousSemigroup X) {omega M : ℝ}
  (hb : S.HasGrowthBound omega M) {lambda : ℝ} (hlambda : omega < lambda) (n : ℕ) :
  ‖S.generator.resolvent lambda ^ n‖ ≤ M / (lambda - omega) ^ n

Lean

Formalized in Tau Ceti as TauCeti.Semigroups.StronglyContinuousSemigroup.norm_generator_resolvent_pow_le.

Sources

• Tau Ceti documentation: TauCeti.Semigroups.StronglyContinuousSemigroup.norm_generator_resolvent_pow_le
• Source of TauCeti.Semigroups.StronglyContinuousSemigroup.norm_generator_resolvent_pow_le in TauCeti/Analysis/Semigroups/Resolvent/PowerBounds.lean

LeanTauCeti.Semigroups.StronglyContinuousSemigroup.norm_generator_resolvent_pow_le

Uses 1 · Used by 1

Proof usesHille–Yosida resolvent bound

Used byHille--Yosida characterization

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.