Multiplication by bounded continuous operator-valued functions on Lᵖ

Let X be a topological space with a Borel measure μ that is inner regular with respect to compact sets on sets of finite measure, for instance the Haar measure MeasureTheory.Measure.haar of a locally compact group. A bounded continuous function F : X →ᵇ (E →L[𝕜] E') acts on Lᵖ(X, E), for 1 ≤ p < ∞, by pointwise application, f ↦ (x ↦ F x (f x)). This file bundles that action as BoundedContinuousFunction.mulLp F μ p hp, a bounded operator of norm at most ‖F‖. When p = 2 and E = E' = H is a Hilbert space, F ↦ F.mulLp μ 2 _ is a unital ⋆-homomorphism BoundedContinuousFunction.mulL2StarAlgHom from X →ᵇ (H →L[𝕜] H) to the bounded operators on L²(X, H). These operators carry the coefficient representation of the regular covariant representation of a C⋆-dynamical system on L²(G, H).

The symbol is not regarded as an element of L∞: on a locally compact group that is not σ-compact, a Haar measure is not σ-finite, and a continuous operator-valued function need not be a.e. strongly measurable. Mathlib's Hölder multiplication ContinuousLinearMap.holderL therefore does not apply. Each f ∈ Lᵖ with p < ∞ vanishes outside a σ-finite set, however, and there inner regularity makes x ↦ F x (f x) a.e. strongly measurable, MeasureTheory.AEFinStronglyMeasurable.aestronglyMeasurable_clm_apply; this is why p = ∞ is excluded. For scalar symbols in L∞ see MeasureTheory.Lp.multiplicationOperator.

theorem BoundedContinuousFunction.memLp_apply {X : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {E' : Type u_4} [TopologicalSpace X] [MeasurableSpace X] [R1Space X] [BorelSpace X] [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {μ : MeasureTheory.Measure X} [μ.InnerRegularCompactLTTop] (F : BoundedContinuousFunction X (E →L[𝕜] E')) {p : ENNReal} (hp₀ : p ≠ 0) (hp : p ≠ ⊤) (f : ↥(MeasureTheory.Lp E p μ)) : MeasureTheory.MemLp (fun (x : X) => (F x) (↑↑f x)) p μ

Pointwise application of a bounded continuous operator-valued function to an Lᵖ function, x ↦ F x (f x), is again in Lᵖ for 0 < p < ∞.

noncomputable def BoundedContinuousFunction.mulLp {X : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {E' : Type u_4} [TopologicalSpace X] [MeasurableSpace X] [R1Space X] [BorelSpace X] [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] (μ : MeasureTheory.Measure X) [μ.InnerRegularCompactLTTop] (p : ENNReal) [Fact (1 ≤ p)] (hp : p ≠ ⊤) (F : BoundedContinuousFunction X (E →L[𝕜] E')) : ↥(MeasureTheory.Lp E p μ) →L[𝕜] ↥(MeasureTheory.Lp E' p μ)

Pointwise application of a bounded continuous operator-valued function F, as a bounded operator f ↦ (x ↦ F x (f x)) from Lᵖ(X, E) to Lᵖ(X, E') for 1 ≤ p < ∞.

theorem BoundedContinuousFunction.coeFn_mulLp {X : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {E' : Type u_4} [TopologicalSpace X] [MeasurableSpace X] [R1Space X] [BorelSpace X] [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {μ : MeasureTheory.Measure X} [μ.InnerRegularCompactLTTop] {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (F : BoundedContinuousFunction X (E →L[𝕜] E')) (f : ↥(MeasureTheory.Lp E p μ)) : ↑↑((mulLp μ p hp F) f) =ᵐ[μ] fun (x : X) => (F x) (↑↑f x)

The multiplication operator acts by pointwise application almost everywhere.

theorem BoundedContinuousFunction.mulLp_eq_iff {X : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {E' : Type u_4} [TopologicalSpace X] [MeasurableSpace X] [R1Space X] [BorelSpace X] [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {μ : MeasureTheory.Measure X} [μ.InnerRegularCompactLTTop] {p : ENNReal} [Fact (1 ≤ p)] {hp : p ≠ ⊤} {F : BoundedContinuousFunction X (E →L[𝕜] E')} {f : ↥(MeasureTheory.Lp E p μ)} {g : ↥(MeasureTheory.Lp E' p μ)} : (mulLp μ p hp F) f = g ↔ (fun (x : X) => (F x) (↑↑f x)) =ᵐ[μ] ↑↑g

Multiplication operators are determined by their pointwise action: an Lᵖ class equal almost everywhere to x ↦ F x (f x) is F.mulLp μ p hp f.

theorem BoundedContinuousFunction.norm_mulLp_le {X : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {E' : Type u_4} [TopologicalSpace X] [MeasurableSpace X] [R1Space X] [BorelSpace X] [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {μ : MeasureTheory.Measure X} [μ.InnerRegularCompactLTTop] {p : ENNReal} [Fact (1 ≤ p)] {hp : p ≠ ⊤} (F : BoundedContinuousFunction X (E →L[𝕜] E')) : ‖mulLp μ p hp F‖ ≤ ‖F‖

The operator norm of a multiplication operator is at most the supremum norm of its symbol.

@[simp]

theorem BoundedContinuousFunction.mulLp_zero {X : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {E' : Type u_4} [TopologicalSpace X] [MeasurableSpace X] [R1Space X] [BorelSpace X] [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {μ : MeasureTheory.Measure X} [μ.InnerRegularCompactLTTop] {p : ENNReal} [Fact (1 ≤ p)] {hp : p ≠ ⊤} : mulLp μ p hp 0 = 0

@[simp]

theorem BoundedContinuousFunction.mulLp_add {X : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {E' : Type u_4} [TopologicalSpace X] [MeasurableSpace X] [R1Space X] [BorelSpace X] [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {μ : MeasureTheory.Measure X} [μ.InnerRegularCompactLTTop] {p : ENNReal} [Fact (1 ≤ p)] {hp : p ≠ ⊤} (F G : BoundedContinuousFunction X (E →L[𝕜] E')) : mulLp μ p hp (F + G) = mulLp μ p hp F + mulLp μ p hp G

@[simp]

theorem BoundedContinuousFunction.mulLp_smul {X : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {E' : Type u_4} [TopologicalSpace X] [MeasurableSpace X] [R1Space X] [BorelSpace X] [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {μ : MeasureTheory.Measure X} [μ.InnerRegularCompactLTTop] {p : ENNReal} [Fact (1 ≤ p)] {hp : p ≠ ⊤} (c : 𝕜) (F : BoundedContinuousFunction X (E →L[𝕜] E')) : mulLp μ p hp (c • F) = c • mulLp μ p hp F

@[simp]

theorem BoundedContinuousFunction.mulLp_one {X : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [TopologicalSpace X] [MeasurableSpace X] [R1Space X] [BorelSpace X] [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {μ : MeasureTheory.Measure X} [μ.InnerRegularCompactLTTop] {p : ENNReal} [Fact (1 ≤ p)] {hp : p ≠ ⊤} : mulLp μ p hp 1 = 1

Multiplication by the constant identity function is the identity operator.

@[simp]

theorem BoundedContinuousFunction.mulLp_mul {X : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [TopologicalSpace X] [MeasurableSpace X] [R1Space X] [BorelSpace X] [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {μ : MeasureTheory.Measure X} [μ.InnerRegularCompactLTTop] {p : ENNReal} [Fact (1 ≤ p)] {hp : p ≠ ⊤} (F G : BoundedContinuousFunction X (E →L[𝕜] E)) : mulLp μ p hp (F * G) = mulLp μ p hp F * mulLp μ p hp G

Multiplication operators compose by pointwise composition of their symbols.

@[simp]

theorem BoundedContinuousFunction.adjoint_mulLp {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [R1Space X] [BorelSpace X] {μ : MeasureTheory.Measure X} [μ.InnerRegularCompactLTTop] {𝕜 : Type u_5} {H : Type u_6} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] (F : BoundedContinuousFunction X (H →L[𝕜] H)) : ContinuousLinearMap.adjoint (mulLp μ 2 ⋯ F) = mulLp μ 2 ⋯ (star F)

The adjoint of multiplication by F is multiplication by the pointwise adjoint star F.

noncomputable def BoundedContinuousFunction.mulL2StarAlgHom {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [R1Space X] [BorelSpace X] (μ : MeasureTheory.Measure X) [μ.InnerRegularCompactLTTop] {𝕜 : Type u_5} {H : Type u_6} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] : BoundedContinuousFunction X (H →L[𝕜] H) →⋆ₐ[𝕜] ↥(MeasureTheory.Lp H 2 μ) →L[𝕜] ↥(MeasureTheory.Lp H 2 μ)

Multiplication of L²(X, H) by bounded continuous operator-valued functions, as a unital ⋆-homomorphism into the bounded operators on L²(X, H).

@[simp]

theorem BoundedContinuousFunction.mulL2StarAlgHom_apply {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [R1Space X] [BorelSpace X] {μ : MeasureTheory.Measure X} [μ.InnerRegularCompactLTTop] {𝕜 : Type u_5} {H : Type u_6} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] (F : BoundedContinuousFunction X (H →L[𝕜] H)) : (mulL2StarAlgHom μ) F = mulLp μ 2 ⋯ F