The multiplication operator M_f on L²

For an essentially bounded measurable scalar function f : α → 𝕜 (i.e. MemLp f ⊤ μ), pointwise multiplication g ↦ f • g is a bounded linear operator on L²(μ), the multiplication operator M_f. Its operator norm is at most the essential supremum ‖f‖∞.

Why this file is here: it is the seed of the multiplication-operator route to the spectral theorem (Pietsch, Operator Ideals, §11.3 — represent S*S as M_f after a unitary change of variables, and read off the spectral projection as M_{𝟙}). That route is not used by the current development: the spectral projection is instead built directly via the continuous functional calculus (Projection) and complexification (RealProjection). This file is kept as a self-contained, independently useful building block for a possible future multiplication-form representation; nothing in the s-numbers chain depends on it.

Main definitions

• MeasureTheory.mulL2 f hf — the multiplication operator M_f : L²(μ) →L[𝕜] L²(μ), g ↦ f • g, for hf : MemLp f ⊤ μ.

Main results

• MeasureTheory.mulL2_coeFn — ⇑(M_f g) =ᵐ[μ] f • ⇑g, the defining a.e. identity (the workhorse for all algebraic properties).
• MeasureTheory.mulL2_opNorm_le — ‖M_f‖ ≤ (eLpNorm f ⊤ μ).toReal.
• MeasureTheory.mulL2_mul — M_f ∘ M_g = M_{f g} (multiplicativity).
• MeasureTheory.mulL2_one — M_1 = id (unitality).
• MeasureTheory.mulL2_isSelfAdjoint — M_f is self-adjoint when f is real-valued; with mulL2_mul this makes an indicator multiplier M_𝟙 an orthogonal projection.

Mathlib reuse: Hölder's inequality for L^∞ · L² (eLpNorm_smul_le_eLpNorm_top_mul_eLpNorm), the MemLp.toLp / MemLp.coeFn_toLp interface to Lp, and LinearMap.mkContinuous.

theorem MeasureTheory.memLp_mul_left {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {𝕜 : Type u_2} [RCLike 𝕜] {f : α → 𝕜} (hf : MemLp f ⊤ μ) (g : ↥(Lp 𝕜 2 μ)) : MemLp (f • ↑↑g) 2 μ

The pointwise product f • g of an essentially bounded f with an L² function g is again in L² (Hölder's inequality with exponents ⊤, 2, 2).

noncomputable def MeasureTheory.mulL2 {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {𝕜 : Type u_2} [RCLike 𝕜] (f : α → 𝕜) (hf : MemLp f ⊤ μ) : ↥(Lp 𝕜 2 μ) →L[𝕜] ↥(Lp 𝕜 2 μ)

The multiplication operator M_f : L²(μ) →L[𝕜] L²(μ), g ↦ f • g, for an essentially bounded measurable scalar function f (hf : MemLp f ⊤ μ).

Equations

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

theorem MeasureTheory.mulL2_coeFn {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {𝕜 : Type u_2} [RCLike 𝕜] (f : α → 𝕜) (hf : MemLp f ⊤ μ) (g : ↥(Lp 𝕜 2 μ)) : ↑↑((mulL2 f hf) g) =ᵐ[μ] f • ↑↑g

Defining identity. As an a.e. function, M_f g is f • g.

theorem MeasureTheory.mulL2_opNorm_le {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {𝕜 : Type u_2} [RCLike 𝕜] (f : α → 𝕜) (hf : MemLp f ⊤ μ) : ‖mulL2 f hf‖ ≤ (eLpNorm f ⊤ μ).toReal

Operator-norm bound. ‖M_f‖ ≤ ‖f‖∞ (the essential supremum of f).

theorem MeasureTheory.memLp_mul_top {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {𝕜 : Type u_2} [RCLike 𝕜] {f g : α → 𝕜} (hf : MemLp f ⊤ μ) (hg : MemLp g ⊤ μ) : MemLp (f * g) ⊤ μ

The product of two essentially bounded functions is essentially bounded.

theorem MeasureTheory.mulL2_mul {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {𝕜 : Type u_2} [RCLike 𝕜] (f g : α → 𝕜) (hf : MemLp f ⊤ μ) (hg : MemLp g ⊤ μ) : mulL2 f hf ∘SL mulL2 g hg = mulL2 (f * g) ⋯

Multiplicativity. M_f ∘ M_g = M_{f g}: multiplication operators compose by multiplying their symbols.

theorem MeasureTheory.mulL2_one {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {𝕜 : Type u_2} [RCLike 𝕜] (h1 : MemLp 1 ⊤ μ) : mulL2 1 h1 = ContinuousLinearMap.id 𝕜 ↥(Lp 𝕜 2 μ)

Unitality. M_1 is the identity operator.

theorem MeasureTheory.mulL2_isSelfAdjoint {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {𝕜 : Type u_2} [RCLike 𝕜] (f : α → 𝕜) (hf : MemLp f ⊤ μ) (hreal : ∀ᵐ (a : α) ∂μ, (starRingEnd 𝕜) (f a) = f a) : IsSelfAdjoint (mulL2 f hf)

Self-adjointness. If the symbol f is real-valued (a.e. fixed by complex conjugation), then M_f is self-adjoint. In particular an indicator symbol gives a self-adjoint operator; together with mulL2_mul (M_𝟙 ∘ M_𝟙 = M_{𝟙·𝟙} = M_𝟙) this makes M_𝟙 an orthogonal projection.

The proof is the pointwise Hölder identity for the L² inner product: ⟪f • x, y⟫ = ∫ conj(f) ⟪x, y⟫ and ⟪x, f • y⟫ = ∫ f ⟪x, y⟫, equal when conj f = f.