Multiplication semigroups on ℓᵖ

For an arbitrary nonnegative multiplier m : ι → ℝ≥0, the operators S(t)x i = exp (-t * m i) * x i form a contraction semigroup on real ℓᵖ, for 1 ≤ p < ∞. No boundedness of m is assumed. Its generator has exactly the natural domain {x | Memℓp (fun i => m i * x i) p} and acts as multiplication by -m. For λ > 0, its resolvent is multiplication by (λ + m)⁻¹.

The finite-exponent hypothesis is essential: unbounded multipliers need not yield strong continuity on ℓ∞.

References

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

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

The contraction semigroup of multiplication by exp (-t * m) on real ℓᵖ, for 1 ≤ p < ∞. The nonnegative multiplier m may be unbounded.

Equations

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

@[simp]

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

Coordinate action of the ℓᵖ multiplication semigroup.

@[simp]

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

The Laplace resolvent acts coordinatewise by multiplication with (λ + m i)⁻¹.

@[simp]

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

The infinitesimal generator of the multiplication semigroup acts coordinatewise as -m. Its domain is characterized by ofLpMultiplication_mem_domain_iff.

@[simp]

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

The generator domain is exactly the vectors whose product with the multiplier is in ℓᵖ. This characterizes the natural domain even when the multiplier is unbounded.

theorem TauCeti.Semigroups.ContractionSemigroup.ofLpMultiplication_not_continuousAt_zero {ι : Type u_1} {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (m : ι → NNReal) (hm : ¬BddAbove (Set.range fun (i : ι) => ↑(m i))) : ¬ContinuousAt (fun (t : NNReal) => (ofLpMultiplication hp m) t) 0

An unbounded nonnegative multiplier gives a semigroup that is not continuous in operator norm at zero, although it is strongly continuous.

theorem TauCeti.Semigroups.ContractionSemigroup.ofLpMultiplication_nat_not_continuousAt_zero {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) : ¬ContinuousAt (fun (t : NNReal) => (ofLpMultiplication hp fun (n : ℕ) => ↑n + 1) t) 0

On ℓᵖ indexed by the natural numbers, the unbounded multiplier m n = n + 1 gives a multiplication contraction semigroup that is not continuous in operator norm at zero.