Multiplication operators on complex L²

An essentially bounded complex function a acts on L² by pointwise multiplication. This file bundles that action as MeasureTheory.Lp.multiplicationOperator a and records its algebraic, adjoint, and norm properties. In particular, on a sigma-finite measure space the operator norm on L² with values in any nontrivial space is exactly the L∞ norm of the symbol, and a symbol of modulus one almost everywhere preserves the L² norm.

The construction is Mathlib's Hölder map for scalar multiplication with one exponent equal to infinity. The resulting operator is the ambient multiplication operator compressed in the definition of a Toeplitz operator.

noncomputable def MeasureTheory.Lp.multiplicationOperator {α : Type u_1} {E : Type u_2} [MeasurableSpace α] {μ : Measure α} [NormedAddCommGroup E] [NormedSpace ℂ E] (a : ↥(Lp ℂ ⊤ μ)) : ↥(Lp E 2 μ) →L[ℂ] ↥(Lp E 2 μ)

Pointwise multiplication by an essentially bounded complex symbol, as a bounded operator on L².

theorem MeasureTheory.Lp.multiplicationOperator_ae {α : Type u_1} {E : Type u_2} [MeasurableSpace α] {μ : Measure α} [NormedAddCommGroup E] [NormedSpace ℂ E] (a : ↥(Lp ℂ ⊤ μ)) (f : ↥(Lp E 2 μ)) : ↑↑((multiplicationOperator a) f) =ᵐ[μ] fun (x : α) => ↑↑a x • ↑↑f x

The multiplication operator acts by pointwise multiplication almost everywhere.

theorem MeasureTheory.Lp.multiplicationOperator_apply {α : Type u_1} {E : Type u_2} [MeasurableSpace α] {μ : Measure α} [NormedAddCommGroup E] [NormedSpace ℂ E] (a : ↥(Lp ℂ ⊤ μ)) (f : ↥(Lp E 2 μ)) : (multiplicationOperator a) f = a • f

Applying the multiplication operator is heterogeneous Lp scalar multiplication.

theorem MeasureTheory.Lp.norm_multiplicationOperator_apply_le {α : Type u_1} {E : Type u_2} [MeasurableSpace α] {μ : Measure α} [NormedAddCommGroup E] [NormedSpace ℂ E] (a : ↥(Lp ℂ ⊤ μ)) (f : ↥(Lp E 2 μ)) : ‖(multiplicationOperator a) f‖ ≤ ‖a‖ * ‖f‖

Multiplication by a changes the L² norm by at most ‖a‖∞.

theorem MeasureTheory.Lp.norm_multiplicationOperator_le {α : Type u_1} {E : Type u_2} [MeasurableSpace α] {μ : Measure α} [NormedAddCommGroup E] [NormedSpace ℂ E] (a : ↥(Lp ℂ ⊤ μ)) : ‖multiplicationOperator a‖ ≤ ‖a‖

The operator norm of multiplication by a is at most its L∞ norm.

@[simp]

theorem MeasureTheory.Lp.multiplicationOperator_zero {α : Type u_1} {E : Type u_2} [MeasurableSpace α] {μ : Measure α} [NormedAddCommGroup E] [NormedSpace ℂ E] : multiplicationOperator 0 = 0

@[simp]

theorem MeasureTheory.Lp.multiplicationOperator_add {α : Type u_1} {E : Type u_2} [MeasurableSpace α] {μ : Measure α} [NormedAddCommGroup E] [NormedSpace ℂ E] (a b : ↥(Lp ℂ ⊤ μ)) : multiplicationOperator (a + b) = multiplicationOperator a + multiplicationOperator b

Multiplication operators depend additively on their symbols.

@[simp]

theorem MeasureTheory.Lp.multiplicationOperator_smul {α : Type u_1} {E : Type u_2} [MeasurableSpace α] {μ : Measure α} [NormedAddCommGroup E] [NormedSpace ℂ E] (c : ℂ) (a : ↥(Lp ℂ ⊤ μ)) : multiplicationOperator (c • a) = c • multiplicationOperator a

Multiplication operators depend complex-linearly on their symbols.

theorem MeasureTheory.Lp.multiplicationOperator_comp_multiplicationOperator {α : Type u_1} {E : Type u_2} [MeasurableSpace α] {μ : Measure α} [NormedAddCommGroup E] [NormedSpace ℂ E] (a b : ↥(Lp ℂ ⊤ μ)) : multiplicationOperator a ∘SL multiplicationOperator b = multiplicationOperator (a * b)

Composing multiplication operators multiplies their symbols in the same order.

theorem MeasureTheory.Lp.commute_multiplicationOperator {α : Type u_1} {E : Type u_2} [MeasurableSpace α] {μ : Measure α} [NormedAddCommGroup E] [NormedSpace ℂ E] (a b : ↥(Lp ℂ ⊤ μ)) : Commute (multiplicationOperator a) (multiplicationOperator b)

Multiplication operators commute with each other.

theorem MeasureTheory.Lp.norm_multiplicationOperator_apply_of_ae_norm_eq_one {α : Type u_1} {E : Type u_2} [MeasurableSpace α] {μ : Measure α} [NormedAddCommGroup E] [NormedSpace ℂ E] {u : ↥(Lp ℂ ⊤ μ)} (hu : ∀ᵐ (x : α) ∂μ, ‖↑↑u x‖ = 1) (f : ↥(Lp E 2 μ)) : ‖(multiplicationOperator u) f‖ = ‖f‖

Multiplication by a symbol of modulus one almost everywhere preserves the L² norm.

theorem MeasureTheory.Lp.multiplicationOperator_of_ae_eq_const {α : Type u_1} {E : Type u_2} [MeasurableSpace α] {μ : Measure α} [NormedAddCommGroup E] [NormedSpace ℂ E] {a : ↥(Lp ℂ ⊤ μ)} {c : ℂ} (ha : ↑↑a =ᵐ[μ] fun (x : α) => c) : multiplicationOperator a = c • ContinuousLinearMap.id ℂ ↥(Lp E 2 μ)

A symbol equal almost everywhere to a constant acts by scalar multiplication.

@[simp]

theorem MeasureTheory.Lp.multiplicationOperator_algebraMap {α : Type u_1} {E : Type u_2} [MeasurableSpace α] {μ : Measure α} [NormedAddCommGroup E] [NormedSpace ℂ E] (c : ℂ) : multiplicationOperator ((algebraMap ℂ ↥(Lp ℂ ⊤ μ)) c) = c • ContinuousLinearMap.id ℂ ↥(Lp E 2 μ)

The scalar embedding into L∞ acts on L² by scalar multiplication.

@[simp]

theorem MeasureTheory.Lp.adjoint_multiplicationOperator {α : Type u_1} {E : Type u_2} [MeasurableSpace α] {μ : Measure α} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (a : ↥(Lp ℂ ⊤ μ)) : ContinuousLinearMap.adjoint (multiplicationOperator a) = multiplicationOperator (star a)

The adjoint of multiplication by a is multiplication by its complex conjugate.

@[simp]

theorem MeasureTheory.Lp.multiplicationOperator_const {α : Type u_1} {E : Type u_2} [MeasurableSpace α] {μ : Measure α} [NormedAddCommGroup E] [NormedSpace ℂ E] [IsFiniteMeasure μ] (c : ℂ) : multiplicationOperator ((Lp.const ⊤ μ) c) = c • ContinuousLinearMap.id ℂ ↥(Lp E 2 μ)

@[simp]

theorem MeasureTheory.Lp.norm_multiplicationOperator {α : Type u_1} {E : Type u_2} [MeasurableSpace α] {μ : Measure α} [NormedAddCommGroup E] [NormedSpace ℂ E] [SigmaFinite μ] [Nontrivial E] (a : ↥(Lp ℂ ⊤ μ)) : ‖multiplicationOperator a‖ = ‖a‖

On a sigma-finite measure space, the operator norm of multiplication by a on L² with values in a nontrivial space is exactly the L∞ norm of a.