Multiplication semigroups with multipliers bounded below

A real multiplier m : ι → ℝ with lower bound a defines the C₀-semigroup S(t)x i = exp (-t * m i) * x i on real ℓᵖ, for 1 ≤ p < ∞. Its growth bound is ‖S(t)‖ ≤ exp (-a * t), so negative values of m are allowed. The generator has domain exactly {x | Memℓp (fun i => m i * x i) p} and acts as -m. For λ > -a, the resolvent is multiplication by (λ + m)⁻¹.

The construction exponentially shifts the contraction semigroup for m - a. The resulting semigroup is independent of the chosen lower bound. Neither the multiplier nor its positive part needs to be bounded; only the lower bound and the finite exponent are required.

References

K.-J. Engel and R. Nagel, One-Parameter Semigroups for Linear Evolution Equations, Section I.4.c (multiplication semigroups).

noncomputable def TauCeti.Semigroups.StronglyContinuousSemigroup.ofLpMultiplication {ι : Type u_1} {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (m : ι → ℝ) (a : ℝ) (hm : ∀ (i : ι), a ≤ m i) : StronglyContinuousSemigroup ↥(lp (fun (x : ι) => ℝ) p)

Multiplication by exp (-t * m) on real ℓᵖ, for a real multiplier with lower bound a. The multiplier may be unbounded above and may take negative values.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.ofLpMultiplication_apply_apply_apply {ι : Type u_1} {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (m : ι → ℝ) (a : ℝ) (hm : ∀ (i : ι), a ≤ m i) (t : NNReal) (x : ↥(lp (fun (x : ι) => ℝ) p)) (i : ι) : ↑(((ofLpMultiplication hp m a hm) t) x) i = Real.exp (-(↑t * m i)) * ↑x i

Coordinate action of the multiplication semigroup with a real multiplier.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.ofLpMultiplication_eq {ι : Type u_1} {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (m : ι → ℝ) (a b : ℝ) (ha : ∀ (i : ι), a ≤ m i) (hb : ∀ (i : ι), b ≤ m i) : ofLpMultiplication hp m a ha = ofLpMultiplication hp m b hb

The multiplication semigroup does not depend on which lower bound is used to construct it.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.ofLpMultiplication_hasGrowthBound {ι : Type u_1} {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (m : ι → ℝ) (a : ℝ) (hm : ∀ (i : ι), a ≤ m i) : (ofLpMultiplication hp m a hm).HasGrowthBound (-a) 1

A lower bound a on the multiplier gives growth exponent -a and growth constant one.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.ofLpMultiplication_generator_apply_apply {ι : Type u_1} {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (m : ι → ℝ) (a : ℝ) (hm : ∀ (i : ι), a ≤ m i) (x : ↥(ofLpMultiplication hp m a hm).generator.domain) (i : ι) : ↑(↑(ofLpMultiplication hp m a hm).generator x) i = -m i * ↑↑x i

The generator acts coordinatewise as multiplication by -m.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.ofLpMultiplication_mem_domain_iff {ι : Type u_1} {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (m : ι → ℝ) (a : ℝ) (hm : ∀ (i : ι), a ≤ m i) (x : ↥(lp (fun (x : ι) => ℝ) p)) : x ∈ (ofLpMultiplication hp m a hm).domain ↔ Memℓp (fun (i : ι) => m i * ↑x i) p

The generator domain is exactly the vectors whose product with m belongs to ℓᵖ. In particular it is independent of the lower bound used in the construction.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.ofLpMultiplication_generator_resolvent_apply_apply {ι : Type u_1} {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (m : ι → ℝ) (a : ℝ) (hm : ∀ (i : ι), a ≤ m i) {c : ℝ} (hc : -a < c) (x : ↥(lp (fun (x : ι) => ℝ) p)) (i : ι) : ↑(((ofLpMultiplication hp m a hm).generator.resolvent c) x) i = (c + m i)⁻¹ * ↑x i

For λ > -a, the resolvent of the generator multiplies each coordinate by (λ + m i)⁻¹.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.ofLpMultiplication_resolvent_apply_apply {ι : Type u_1} {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (m : ι → ℝ) (a : ℝ) (hm : ∀ (i : ι), a ≤ m i) {c : ℝ} (hc : -a < c) (x : ↥(lp (fun (x : ι) => ℝ) p)) (i : ι) : ↑(((ofLpMultiplication hp m a hm).resolvent ⋯ c hc) x) i = (c + m i)⁻¹ * ↑x i

The pointwise Laplace resolvent has the same explicit formula above the growth exponent.