The multiplication semigroup on bounded continuous functions

For a bounded continuous multiplier m : α →ᵇ ℝ this file constructs the multiplication semigroup on the Banach space α →ᵇ ℝ of bounded continuous real functions:

S(t) f = e^{-t·m} · f, acting by pointwise multiplication.

This is the remaining concrete acceptance example for Part A of the one-parameter-semigroups roadmap. It is the bounded-operator semigroup ofBounded generated by multiplication by -m, and we develop:

• StronglyContinuousSemigroup.ofMultiplication m: the C₀-semigroup t ↦ multiplication by e^{-t·m}, with growth bound (‖m⁻‖, 1) controlled by the negative part of m;
• its generator: the domain is the whole space and the generator is multiplication by -m (ofMultiplication_domain_eq_top, ofMultiplication_generator);
• its resolvent: for ‖m⁻‖ < λ the Laplace-transform resolvent acts as multiplication by the pointwise inverse (λ + m)⁻¹ (ofMultiplication_resolvent_eq), which identifies it with the resolvent of the generator through the bridge lemma generator_resolvent_eq (ofMultiplication_generator_resolvent_eq);
• ContractionSemigroup.ofMultiplication: when 0 ≤ m the semigroup is contractive, so the abstract bound ‖R(λ)‖ ≤ 1/λ applies to it concretely.

References

The multiplication semigroup is the standard first example of a C₀-semigroup; see Engel--Nagel, One-Parameter Semigroups for Linear Evolution Equations, Ch. I, and Pazy, Semigroups of Linear Operators, Ch. 1.

The exponential multiplier

noncomputable def TauCeti.BoundedContinuousFunction.expNegMul {α : Type u_1} [TopologicalSpace α] (t : ℝ) (m : BoundedContinuousFunction α ℝ) : BoundedContinuousFunction α ℝ

The exponential multiplier x ↦ exp (-t · m x) as a bounded continuous function.

Equations

• TauCeti.BoundedContinuousFunction.expNegMul t m = BoundedContinuousFunction.ofNormedAddCommGroup (fun (x : α) => Real.exp (-(t * m x))) ⋯ (Real.exp (|t| * ‖m‖)) ⋯

@[simp]

theorem TauCeti.BoundedContinuousFunction.coe_expNegMul {α : Type u_1} [TopologicalSpace α] (t : ℝ) (m : BoundedContinuousFunction α ℝ) : ⇑(expNegMul t m) = fun (x : α) => Real.exp (-(t * m x))

The coercion of expNegMul t m is the function x ↦ exp (-(t * m x)).

theorem TauCeti.BoundedContinuousFunction.exp_apply {α : Type u_1} [TopologicalSpace α] (g : BoundedContinuousFunction α ℝ) (x : α) : (NormedSpace.exp g) x = Real.exp (g x)

Evaluation of the Banach-algebra exponential of a bounded continuous real function.

theorem TauCeti.BoundedContinuousFunction.norm_expNegMul_le {α : Type u_1} [TopologicalSpace α] {t : ℝ} (ht : 0 ≤ t) (m : BoundedContinuousFunction α ℝ) : ‖expNegMul t m‖ ≤ Real.exp (t * ‖m⁻‖)

For t ≥ 0, the exponential multiplier is bounded by e^{t ‖m⁻‖}.

The multiplication semigroup

noncomputable def TauCeti.Semigroups.StronglyContinuousSemigroup.ofMultiplication {α : Type u_1} [TopologicalSpace α] (m : BoundedContinuousFunction α ℝ) : StronglyContinuousSemigroup (BoundedContinuousFunction α ℝ)

The multiplication semigroup: for a bounded continuous multiplier m, the C₀-semigroup on the Banach space α →ᵇ ℝ generated by multiplication by -m. It is the bounded-operator semigroup ofBounded (ContinuousLinearMap.mul ℝ (α →ᵇ ℝ) (-m)), and acts by pointwise multiplication with exp (-t·m), that is S(t) f = e^{-t·m} · f. For λ > ‖m⁻‖ its resolvent acts as multiplication by the pointwise inverse (λ + m)⁻¹ (ofMultiplication_resolvent_eq).

Equations

• TauCeti.Semigroups.StronglyContinuousSemigroup.ofMultiplication m = TauCeti.Semigroups.StronglyContinuousSemigroup.ofBounded ((ContinuousLinearMap.mul ℝ (BoundedContinuousFunction α ℝ)) (-m))

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.ofMultiplication_eq_ofBounded {α : Type u_1} [TopologicalSpace α] (m : BoundedContinuousFunction α ℝ) : ofMultiplication m = ofBounded ((ContinuousLinearMap.mul ℝ (BoundedContinuousFunction α ℝ)) (-m))

The multiplication semigroup is the bounded-generator semigroup for multiplication by -m.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.ofMultiplication_apply {α : Type u_1} [TopologicalSpace α] (m : BoundedContinuousFunction α ℝ) (t : NNReal) : (ofMultiplication m) t = (ContinuousLinearMap.mul ℝ (BoundedContinuousFunction α ℝ)) (BoundedContinuousFunction.expNegMul (↑t) m)

The operator of the multiplication semigroup at time t is multiplication by e^{-t·m}.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.ofMultiplication_apply_apply {α : Type u_1} [TopologicalSpace α] (m : BoundedContinuousFunction α ℝ) (t : NNReal) (f : BoundedContinuousFunction α ℝ) : ((ofMultiplication m) t) f = BoundedContinuousFunction.expNegMul (↑t) m * f

The multiplication semigroup at time t acts on f by multiplication with e^{-t·m}.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.ofMultiplication_apply_apply_apply {α : Type u_1} [TopologicalSpace α] (m : BoundedContinuousFunction α ℝ) (t : NNReal) (f : BoundedContinuousFunction α ℝ) (x : α) : (((ofMultiplication m) t) f) x = Real.exp (-(↑t * m x)) * f x

Pointwise action of the multiplication semigroup: (S(t) f)(x) = e^{-t·m x} · f(x).

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.ofMultiplication_realOperator_of_nonneg {α : Type u_1} [TopologicalSpace α] (m : BoundedContinuousFunction α ℝ) {t : ℝ} (ht : 0 ≤ t) : (ofMultiplication m).realOperator t = (ContinuousLinearMap.mul ℝ (BoundedContinuousFunction α ℝ)) (BoundedContinuousFunction.expNegMul t m)

The real-time operator of the multiplication semigroup at t ≥ 0 is multiplication by e^{-t·m}.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.ofMultiplication_hasGrowthBound {α : Type u_1} [TopologicalSpace α] (m : BoundedContinuousFunction α ℝ) : (ofMultiplication m).HasGrowthBound ‖m⁻‖ 1

The multiplication semigroup has growth bound (‖m⁻‖, 1).

The generator

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.ofMultiplication_domain_eq_top {α : Type u_1} [TopologicalSpace α] (m : BoundedContinuousFunction α ℝ) : (ofMultiplication m).domain = ⊤

The generator domain of the multiplication semigroup is the whole space.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.ofMultiplication_generator {α : Type u_1} [TopologicalSpace α] (m : BoundedContinuousFunction α ℝ) : (ofMultiplication m).generator = (↑((ContinuousLinearMap.mul ℝ (BoundedContinuousFunction α ℝ)) (-m))).toPMap ⊤

The generator of the multiplication semigroup is multiplication by -m, on the whole space.

The concrete resolvent

noncomputable def TauCeti.BoundedContinuousFunction.addInv {α : Type u_1} [TopologicalSpace α] (c : ℝ) (m : BoundedContinuousFunction α ℝ) (hc : ‖m⁻‖ < c) : BoundedContinuousFunction α ℝ

The pointwise inverse (c + m)⁻¹ of a positive perturbation of a bounded continuous multiplier, as bounded continuous function. The hypothesis ‖m⁻‖ < c guarantees c + m x ≥ c - ‖m⁻‖ > 0 for every x.

Equations

• TauCeti.BoundedContinuousFunction.addInv c m hc = BoundedContinuousFunction.ofNormedAddCommGroup (fun (x : α) => (c + m x)⁻¹) ⋯ (1 / (c - ‖m⁻‖)) ⋯

@[simp]

theorem TauCeti.BoundedContinuousFunction.coe_addInv {α : Type u_1} [TopologicalSpace α] (c : ℝ) (m : BoundedContinuousFunction α ℝ) (hc : ‖m⁻‖ < c) : ⇑(addInv c m hc) = fun (x : α) => (c + m x)⁻¹

The coercion of addInv c m hc is the function x ↦ (c + m x)⁻¹.

theorem TauCeti.BoundedContinuousFunction.norm_addInv_le {α : Type u_1} [TopologicalSpace α] (c : ℝ) (m : BoundedContinuousFunction α ℝ) (hc : ‖m⁻‖ < c) : ‖addInv c m hc‖ ≤ 1 / (c - ‖m⁻‖)

The pointwise inverse (c + m)⁻¹ has norm at most 1 / (c - ‖m⁻‖).

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.ofMultiplication_resolvent_eq {α : Type u_1} [TopologicalSpace α] (m : BoundedContinuousFunction α ℝ) {c : ℝ} (hc : ‖m⁻‖ < c) : (ofMultiplication m).resolvent ⋯ c hc = (ContinuousLinearMap.mul ℝ (BoundedContinuousFunction α ℝ)) (BoundedContinuousFunction.addInv c m hc)

The resolvent of the multiplication semigroup: for ‖m⁻‖ < λ, the Laplace-transform resolvent acts as multiplication by the pointwise inverse (λ + m)⁻¹, that is R(λ) f = (λ + m)⁻¹ · f.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.ofMultiplication_generator_resolvent_eq {α : Type u_1} [TopologicalSpace α] (m : BoundedContinuousFunction α ℝ) {c : ℝ} (hc : ‖m⁻‖ < c) : (ofMultiplication m).generator.resolvent c = (ContinuousLinearMap.mul ℝ (BoundedContinuousFunction α ℝ)) (BoundedContinuousFunction.addInv c m hc)

Through the bridge lemma generator_resolvent_eq, the concrete formula identifies the resolvent of the generator: it is multiplication by the pointwise inverse (λ + m)⁻¹ for λ > ‖m⁻‖.

The contraction case

noncomputable def TauCeti.Semigroups.ContractionSemigroup.ofMultiplication {α : Type u_1} [TopologicalSpace α] (m : BoundedContinuousFunction α ℝ) (hm : 0 ≤ m) : ContractionSemigroup (BoundedContinuousFunction α ℝ)

For a nonnegative multiplier m ≥ 0, the multiplication semigroup is contractive; in particular the abstract bound ContractionSemigroup.resolvent_norm_le applies to it, giving the concrete estimate ‖R(λ)‖ ≤ 1/λ for λ > 0.

Equations

• TauCeti.Semigroups.ContractionSemigroup.ofMultiplication m hm = { toStronglyContinuousSemigroup := TauCeti.Semigroups.StronglyContinuousSemigroup.ofMultiplication m, contracting := ⋯ }

@[simp]

theorem TauCeti.Semigroups.ContractionSemigroup.ofMultiplication_toStronglyContinuousSemigroup {α : Type u_1} [TopologicalSpace α] (m : BoundedContinuousFunction α ℝ) (hm : 0 ≤ m) : (ofMultiplication m hm).toStronglyContinuousSemigroup = StronglyContinuousSemigroup.ofMultiplication m

The C₀-semigroup underlying the multiplication contraction semigroup is the multiplication semigroup.

@[simp]

theorem TauCeti.Semigroups.ContractionSemigroup.ofMultiplication_apply {α : Type u_1} [TopologicalSpace α] (m : BoundedContinuousFunction α ℝ) (hm : 0 ≤ m) (t : NNReal) : (ofMultiplication m hm) t = (ContinuousLinearMap.mul ℝ (BoundedContinuousFunction α ℝ)) (BoundedContinuousFunction.expNegMul (↑t) m)

The operator of the multiplication contraction semigroup at time t is multiplication by e^{-t·m}.

theorem TauCeti.Semigroups.ContractionSemigroup.ofMultiplication_apply_apply {α : Type u_1} [TopologicalSpace α] (m : BoundedContinuousFunction α ℝ) (hm : 0 ≤ m) (t : NNReal) (f : BoundedContinuousFunction α ℝ) : ((ofMultiplication m hm) t) f = BoundedContinuousFunction.expNegMul (↑t) m * f

The multiplication contraction semigroup acts on f by multiplication with e^{-t·m}.

theorem TauCeti.Semigroups.ContractionSemigroup.ofMultiplication_apply_apply_apply {α : Type u_1} [TopologicalSpace α] (m : BoundedContinuousFunction α ℝ) (hm : 0 ≤ m) (t : NNReal) (f : BoundedContinuousFunction α ℝ) (x : α) : (((ofMultiplication m hm) t) f) x = Real.exp (-(↑t * m x)) * f x

Pointwise action of the multiplication contraction semigroup.

theorem TauCeti.Semigroups.ContractionSemigroup.ofMultiplication_resolvent_eq {α : Type u_1} [TopologicalSpace α] (m : BoundedContinuousFunction α ℝ) (hm : 0 ≤ m) {c : ℝ} (hc : 0 < c) : (ofMultiplication m hm).resolvent c hc = (ContinuousLinearMap.mul ℝ (BoundedContinuousFunction α ℝ)) (BoundedContinuousFunction.addInv c m ⋯)

The resolvent of the multiplication contraction semigroup is multiplication by (c + m)⁻¹.