Multiplication operators on L²

Category: 1-Mathlib (CSD-free; staged for upstream).

DiagonalOperator.lean (BACKLOG #93(a)) builds the unbounded-operator layer the pin lacks — LinearPMap.IsResolventAt, resolventSet, spectrum — and the one operator a Hilbert basis supplies: the diagonal operator of a real weight family, self-adjoint with spectrum the closure of the weights. That route needs a basis, so it reaches only operators with discrete spectrum. This module is its continuum companion: multiplication by a real measurable function on L²(μ), where the spectrum is in general not discrete.

• the bounded part first: mulCLM is multiplication by a bounded measurable function, through Mathlib's Hölder pairing L^∞ × L² → L² (the function-indexed companion of HeatSemigroup.lean's potential), and cutCLM, cutMulCLM are the cut-offs 1_{|m| ≤ n} and m · 1_{|m| ≤ n};
• ★ ae_eq_zero_of_ae_eq_zero_on_cutSet — the cut-offs exhaust α, because m is real-valued: a function vanishing a.e. on every cut-off set vanishes a.e. This one lemma replaces every limiting argument below — no dominated convergence appears in this file;
• mulDomain, mulOp — the natural domain {f ∈ L² : m f ∈ L²} and the operator on it;
• ★★ dense_mulDomain — the domain is dense: a vector orthogonal to it is killed by every cut-off (the cut-offs are self-adjoint, inner_cutCLM), hence vanishes;
• ★★ mulOp_isFormalAdjoint — symmetry, the one place reality of m is used; and the content, ★★★ isSelfAdjoint_mulOp — multiplication by a real measurable function is self-adjoint on its natural domain. Maximality is coeFn_adjoint_mulOp: the adjoint's value agrees with m · y on every cut-off set, so a vector the adjoint is defined at already has m · y ∈ L²;
• ★★ mem_resolventSet_mulOp — off the closure of the values the operator has a bounded inverse, multiplication by (m − z)⁻¹; m/(m − z) is bounded too, which is what puts the inverse's values back in the domain;
• ★★ mem_spectrum_mulOp — every essential value is in the spectrum: the normalised indicators of m⁻¹(ball λ ε) are approximate eigenvectors, so a bounded inverse would have to stretch one of them by more than its own norm. Together with the previous item this pins the spectrum between the essential values and the closure of all values.

Honest scope

⚠️ m is real, which is what makes the operator self-adjoint; a complex multiplier gives a normal operator and nothing here is stated for that case.

⚠️ No spectral theorem and no functional calculus. The spectrum is characterised by the two one-sided statements above, not computed in general: identifying it with the essential range needs the measure, which is done for the free Hamiltonian in ../Semigroup/FreeHamiltonian.lean and not in general. There is no projection-valued measure here (MATHLIB-ABSENT(LinearPMap.spectralMeasure)), and Mathlib has no multiplication operator on Lp to build on (MATHLIB-ABSENT(MeasureTheory.multiplicationOperator)).

⚠️ Nothing about generated groups. Stone's theorem is absent from the pin (MATHLIB-ABSENT(LinearPMap.stoneTheorem)), so no statement here connects a self-adjoint operator to a one-parameter unitary group; the corpus's propagators are built directly as Fourier multipliers.

References: M. Reed, B. Simon, Methods of Modern Mathematical Physics I §VII.2 and §VIII.3 (the multiplication operator and its spectrum); DiagonalOperator.lean (BACKLOG #93(a)); specs/BACKLOG.md #64; specs/future-work.md.

Multiplication by a bounded function

noncomputable def MeasureTheory.L2.mulCLM {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (g : α → ℂ) (hg : AEStronglyMeasurable g μ) {C : ℝ} (hb : ∀ᵐ (x : α) ∂μ, ‖g x‖ ≤ C) : ↥(Lp ℂ 2 μ) →L[ℂ] ↥(Lp ℂ 2 μ)

Multiplication by a bounded measurable function as an operator on L², through Mathlib's Hölder pairing L^∞ × L² → L². This is the function-indexed companion of Analysis/Semigroup/HeatSemigroup.lean's potential, which takes an L^∞ element; here the bound is a hypothesis, which is what the cut-offs below need.

Equations

• MeasureTheory.L2.mulCLM g hg hb = (ContinuousLinearMap.holderL μ ⊤ 2 2 (ContinuousLinearMap.mul ℂ ℂ)) (MeasureTheory.MemLp.toLp g ⋯)

theorem MeasureTheory.L2.coeFn_mulCLM {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (g : α → ℂ) (hg : AEStronglyMeasurable g μ) {C : ℝ} (hb : ∀ᵐ (x : α) ∂μ, ‖g x‖ ≤ C) (f : ↥(Lp ℂ 2 μ)) : ↑↑((mulCLM g hg hb) f) =ᵐ[μ] fun (x : α) => g x * ↑↑f x

The cut-offs

def MeasureTheory.L2.cutSet {α : Type u_1} (m : α → ℝ) (n : ℕ) : Set α

The cut-off set {|m| ≤ n}. The cut-offs exhaust α because m is real-valued, and that is the only property of them used below.

Equations

• MeasureTheory.L2.cutSet m n = {x : α | |m x| ≤ ↑n}

theorem MeasureTheory.L2.measurableSet_cutSet {α : Type u_1} [MeasurableSpace α] {m : α → ℝ} (hm : Measurable m) (n : ℕ) : MeasurableSet (cutSet m n)

theorem MeasureTheory.L2.exists_mem_cutSet {α : Type u_1} {m : α → ℝ} (x : α) : ∃ (n : ℕ), x ∈ cutSet m n

theorem MeasureTheory.L2.aestronglyMeasurable_indicator_cutSet {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {m : α → ℝ} (hm : Measurable m) (n : ℕ) : AEStronglyMeasurable ((cutSet m n).indicator fun (x : α) => 1) μ

theorem MeasureTheory.L2.norm_indicator_cutSet_le {α : Type u_1} {m : α → ℝ} (n : ℕ) (x : α) : ‖(cutSet m n).indicator (fun (x : α) => 1) x‖ ≤ 1

theorem MeasureTheory.L2.aestronglyMeasurable_indicator_cutSet_mul {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {m : α → ℝ} (hm : Measurable m) (n : ℕ) : AEStronglyMeasurable ((cutSet m n).indicator fun (x : α) => ↑(m x)) μ

theorem MeasureTheory.L2.norm_indicator_cutSet_mul_le {α : Type u_1} {m : α → ℝ} (n : ℕ) (x : α) : ‖(cutSet m n).indicator (fun (x : α) => ↑(m x)) x‖ ≤ ↑n

noncomputable def MeasureTheory.L2.cutCLM {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {m : α → ℝ} (hm : Measurable m) (n : ℕ) : ↥(Lp ℂ 2 μ) →L[ℂ] ↥(Lp ℂ 2 μ)

Multiplication by the cut-off indicator 1_{|m| ≤ n}.

Equations

• MeasureTheory.L2.cutCLM hm n = MeasureTheory.L2.mulCLM ((MeasureTheory.L2.cutSet m n).indicator fun (x : α) => 1) ⋯ ⋯

theorem MeasureTheory.L2.coeFn_cutCLM {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {m : α → ℝ} (hm : Measurable m) (n : ℕ) (f : ↥(Lp ℂ 2 μ)) : ↑↑((cutCLM hm n) f) =ᵐ[μ] fun (x : α) => (cutSet m n).indicator (fun (x : α) => 1) x * ↑↑f x

noncomputable def MeasureTheory.L2.cutMulCLM {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {m : α → ℝ} (hm : Measurable m) (n : ℕ) : ↥(Lp ℂ 2 μ) →L[ℂ] ↥(Lp ℂ 2 μ)

Multiplication by m cut off at n: bounded, hence defined on all of L².

Equations

• MeasureTheory.L2.cutMulCLM hm n = MeasureTheory.L2.mulCLM ((MeasureTheory.L2.cutSet m n).indicator fun (x : α) => ↑(m x)) ⋯ ⋯

theorem MeasureTheory.L2.coeFn_cutMulCLM {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {m : α → ℝ} (hm : Measurable m) (n : ℕ) (f : ↥(Lp ℂ 2 μ)) : ↑↑((cutMulCLM hm n) f) =ᵐ[μ] fun (x : α) => (cutSet m n).indicator (fun (x : α) => ↑(m x)) x * ↑↑f x

theorem MeasureTheory.L2.ae_eq_zero_of_ae_eq_zero_on_cutSet {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {m : α → ℝ} {u : α → ℂ} (h : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, x ∈ cutSet m n → u x = 0) : u =ᵐ[μ] 0

The cut-offs exhaust α: a function vanishing a.e. on every cut-off set vanishes a.e. This replaces a dominated-convergence argument everywhere below.

The unbounded multiplication operator

def MeasureTheory.L2.mulDomain {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (m : α → ℝ) : Submodule ℂ ↥(Lp ℂ 2 μ)

The natural domain of multiplication by m: those f ∈ L² whose product with m is in L².

Equations

• MeasureTheory.L2.mulDomain m = { carrier := {f : ↥(MeasureTheory.Lp ℂ 2 μ) | MeasureTheory.MemLp (fun (x : α) => ↑(m x) * ↑↑f x) 2 μ}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem MeasureTheory.L2.mem_mulDomain_iff {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {m : α → ℝ} {f : ↥(Lp ℂ 2 μ)} : f ∈ mulDomain m ↔ MemLp (fun (x : α) => ↑(m x) * ↑↑f x) 2 μ

noncomputable def MeasureTheory.L2.mulVal {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {m : α → ℝ} (f : ↥(mulDomain m)) : ↥(Lp ℂ 2 μ)

The value of the multiplication operator, as an L² element. Wrapping the toLp in a definition keeps its MemLp proof opaque, so the rewriting below matches syntactically.

Equations

• MeasureTheory.L2.mulVal f = MeasureTheory.MemLp.toLp (fun (x : α) => ↑(m x) * ↑↑↑f x) ⋯

theorem MeasureTheory.L2.coeFn_mulVal {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {m : α → ℝ} (f : ↥(mulDomain m)) : ↑↑(mulVal f) =ᵐ[μ] fun (x : α) => ↑(m x) * ↑↑↑f x

theorem MeasureTheory.L2.mulVal_add {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {m : α → ℝ} (f g : ↥(mulDomain m)) : mulVal (f + g) = mulVal f + mulVal g

theorem MeasureTheory.L2.mulVal_smul {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {m : α → ℝ} (c : ℂ) (f : ↥(mulDomain m)) : mulVal (c • f) = c • mulVal f

noncomputable def MeasureTheory.L2.mulOp {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (m : α → ℝ) : ↥(Lp ℂ 2 μ) →ₗ.[ℂ] ↥(Lp ℂ 2 μ)

Multiplication by a real measurable function as an unbounded operator on L², on its natural domain.

Equations

• MeasureTheory.L2.mulOp m = { domain := MeasureTheory.L2.mulDomain m, toFun := { toFun := MeasureTheory.L2.mulVal, map_add' := ⋯, map_smul' := ⋯ } }

@[simp]

theorem MeasureTheory.L2.mulOp_domain {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {m : α → ℝ} : (mulOp m).domain = mulDomain m

theorem MeasureTheory.L2.mulOp_apply {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {m : α → ℝ} (f : ↥(mulOp m).domain) : ↑(mulOp m) f = mulVal f

theorem MeasureTheory.L2.coeFn_mulOp {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {m : α → ℝ} (f : ↥(mulOp m).domain) : ↑↑(↑(mulOp m) f) =ᵐ[μ] fun (x : α) => ↑(m x) * ↑↑↑f x

theorem MeasureTheory.L2.cutCLM_mem_mulDomain {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {m : α → ℝ} (hm : Measurable m) (n : ℕ) (k : ↥(Lp ℂ 2 μ)) : (cutCLM hm n) k ∈ mulDomain m

Every cut-off of every L² function lies in the domain: the cut-off makes m bounded.

The cut-off is self-adjoint

theorem MeasureTheory.L2.conj_indicator_cutSet {α : Type u_1} {m : α → ℝ} (n : ℕ) (x : α) : (starRingEnd ℂ) ((cutSet m n).indicator (fun (x : α) => 1) x) = (cutSet m n).indicator (fun (x : α) => 1) x

theorem MeasureTheory.L2.indicator_cutSet_mul {α : Type u_1} {m : α → ℝ} (n : ℕ) (x : α) : (cutSet m n).indicator (fun (x : α) => ↑(m x)) x = (cutSet m n).indicator (fun (x : α) => 1) x * ↑(m x)

theorem MeasureTheory.L2.inner_cutCLM {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {m : α → ℝ} (hm : Measurable m) (n : ℕ) (f g : ↥(Lp ℂ 2 μ)) : inner ℂ ((cutCLM hm n) f) g = inner ℂ f ((cutCLM hm n) g)

The cut-off is a self-adjoint bounded operator: it moves across the inner product.

theorem MeasureTheory.L2.dense_mulDomain {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {m : α → ℝ} (hm : Measurable m) : Dense ↑(mulDomain m)

★★ The domain is dense. A vector orthogonal to it is killed by every cut-off, hence vanishes a.e. on every cut-off set, and the cut-offs exhaust α: no approximation argument is needed.

Symmetry and self-adjointness

theorem MeasureTheory.L2.mulOp_isFormalAdjoint {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (m : α → ℝ) : (mulOp m).IsFormalAdjoint (mulOp m)

★★ Multiplication by a real function is symmetric: the factor comes out of either slot unchanged, which is the only place reality of m is used.

theorem MeasureTheory.L2.isSymmetric_mulCLM {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (g : α → ℝ) (hg : AEStronglyMeasurable (fun (x : α) => ↑(g x)) μ) {C : ℝ} (hb : ∀ᵐ (x : α) ∂μ, ‖↑(g x)‖ ≤ C) : (↑(mulCLM (fun (x : α) => ↑(g x)) hg hb)).IsSymmetric

★★ Multiplication by a bounded real function is symmetric as a bounded operator — the hypothesis #64(ii)'s perturbation theorem consumes, discharged here for the only perturbation the corpus needs. Reality of the function is the whole of it, exactly as for the unbounded mulOp.

theorem MeasureTheory.L2.inner_cutMulCLM {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {m : α → ℝ} (hm : Measurable m) (n : ℕ) (k y : ↥(Lp ℂ 2 μ)) : inner ℂ ((cutMulCLM hm n) y) k = inner ℂ y (↑(mulOp m) ⟨(cutCLM hm n) k, ⋯⟩)

Pairing the operator against a cut-off moves the cut-off m to the other slot.

theorem MeasureTheory.L2.coeFn_adjoint_mulOp {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {m : α → ℝ} (hm : Measurable m) (y : ↥(mulOp m).adjoint.domain) : ↑↑(↑(mulOp m).adjoint y) =ᵐ[μ] fun (x : α) => ↑(m x) * ↑↑↑y x

The adjoint multiplies by m too: on every cut-off set its value agrees with m · y, and the cut-offs exhaust α. This is the computation behind maximality.

theorem MeasureTheory.L2.isSelfAdjoint_mulOp {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {m : α → ℝ} (hm : Measurable m) : IsSelfAdjoint (mulOp m)

★★★ Multiplication by a real measurable function is self-adjoint on its natural domain. Symmetry is the easy half; the content is maximality — a vector the adjoint is defined at already has m · y ∈ L², because the adjoint's value is m · y on every cut-off set.

The resolvent

theorem MeasureTheory.L2.mem_resolventSet_mulOp {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {m : α → ℝ} (hm : Measurable m) {z : ℂ} (hz : z ∉ closure (Set.range fun (x : α) => ↑(m x))) : z ∈ (mulOp m).resolventSet

★★ Off the closure of the values, multiplication by m has a bounded inverse, namely multiplication by (m − z)⁻¹. The reciprocal is bounded there — that is what being off the closure says — and m/(m − z) is bounded too, which is what puts the inverse's values back in the domain.

The spectrum

theorem MeasureTheory.L2.mem_spectrum_mulOp {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {m : α → ℝ} (hm : Measurable m) {lam : ℝ} (hpos : ∀ (ε : ℝ), 0 < ε → μ (m ⁻¹' Metric.ball lam ε) ≠ 0) (hfin : ∀ (ε : ℝ), 0 < ε → μ (m ⁻¹' Metric.ball lam ε) ≠ ⊤) : ↑lam ∈ (mulOp m).spectrum

★★ Every value that m takes on sets of positive measure is in the spectrum. The normalised indicators of the preimages m⁻¹(ball lam ε) are approximate eigenvectors: (M_m − lam) shrinks them by ε, so a bounded inverse would have to stretch one of them by more than its own norm. The two hypotheses say exactly that lam is an essential value of m.