Multiplication operators on L²

DefinitionEssential range#✓fully proved

Let \(\mu\) be a measure on a measurable space \(\alpha\) and let \(\varphi : \alpha \to \mathbb{C}\). The essential range of \(\varphi\) with respect to \(\mu\) is the set of \(z \in \mathbb{C}\) such that \(\mu(\{x \in \alpha : |\varphi(x) - z| < \varepsilon\}) > 0\) for every \(\varepsilon > 0\).

def essentialRange (φ : α → ℂ) (μ : Measure α) : Set ℂ :=
  {z | ∀ ε > 0, 0 < μ (φ ⁻¹' Metric.ball z ε)}

Used by 6

Used byThe essential range is invariant under almost-everywhere equality · Essential range of a constant function · Essential range for counting measure on a finite type · Points outside the essential range · Spectrum of a multiplication operator on L² · Spectrum of an L² multiplication operator with measurable multiplier

TheoremThe essential range is invariant under almost-everywhere equality#✓fully proved

Let \(\mu\) be a measure on a measurable space \(\alpha\) and let \(\varphi, \psi : \alpha \to \mathbb{C}\). If \(\varphi = \psi\) \(\mu\)-almost everywhere, then \(\varphi\) and \(\psi\) have the same essential range with respect to \(\mu\).

theorem essentialRange_congr_ae {φ ψ : α → ℂ} (h : φ =ᵐ[μ] ψ) :
    essentialRange φ μ = essentialRange ψ μ

Uses 1 · Used by 1

Statement usesEssential range

Used bySpectrum of a multiplication operator on L²

TheoremPoints outside the essential range#✓fully proved

Let \(\mu\) be a measure on a measurable space \(\alpha\), let \(\varphi : \alpha \to \mathbb{C}\) and let \(z \in \mathbb{C}\). Then \(z\) is not in the essential range of \(\varphi\) with respect to \(\mu\) if and only if there is \(\varepsilon > 0\) such that the preimage under \(\varphi\) of the open ball \(B(z, \varepsilon) = \{w \in \mathbb{C} : |w - z| < \varepsilon\}\) has \(\mu\)-measure zero.

theorem not_mem_essentialRange_iff {φ : α → ℂ} {z : ℂ} :
    z ∉ essentialRange φ μ ↔ ∃ ε > 0, μ (φ ⁻¹' Metric.ball z ε) = 0

Uses 1 · Used by 1

Statement usesEssential range

Used bySpectrum of an L² multiplication operator with measurable multiplier

TheoremEssential range of a constant function#✓fully proved

Let \(\mu\) be a measure on a measurable space \(\alpha\) with \(\mu(\alpha) \neq 0\), and let \(c \in \mathbb{C}\). Then the essential range of the constant function \(x \mapsto c\) with respect to \(\mu\) is \(\{c\}\).

theorem essentialRange_const {c : ℂ} (hμ : μ univ ≠ 0) :
    essentialRange (fun _ => c) μ = {c}

Uses 1

Statement usesEssential range

TheoremEssential range for counting measure on a finite type#✓fully proved

Let \(\alpha\) be a finite type with a measurable structure in which singletons are measurable, and let \(\varphi : \alpha \to \mathbb{C}\). Then the essential range of \(\varphi\) with respect to counting measure on \(\alpha\) is the range \(\varphi(\alpha)\).

theorem essentialRange_count_eq_range [Finite α] [MeasurableSingletonClass α]
    (φ : α → ℂ) :
    essentialRange φ (Measure.count : Measure α) = Set.range φ

Uses 1

Statement usesEssential range

TheoremAn essentially bounded multiple of an \(L^2\) function is in \(L^2\)#✓fully proved

Let \(\mu\) be a measure on a measurable space \(\alpha\), let \(\varphi \colon \alpha \to \mathbb{C}\) be an essentially bounded, almost everywhere strongly measurable function, and let \(f \in L^2(\mu)\). Then the pointwise product \(x \mapsto \varphi(x) f(x)\), formed with a representative of \(f\), belongs to \(\mathcal{L}^2(\mu)\): it is almost everywhere strongly measurable and square integrable.

theorem memLp_mul_of_memLp_top {φ : α → ℂ} (hφ : MemLp φ ∞ μ)
    (f : Lp ℂ 2 μ) : MemLp (fun x => φ x * f x) 2 μ

Used by 9

Used byShifting a multiplication operator by a scalar · Eigenvalues of a multiplication operator on \(L^2\), measurable multiplier · Lower bound for the norm of a multiplication operator · Multiplication operator on \(L^2\) · Multiplication operators with almost everywhere equal multipliers coincide · Multiplication by a constant function on \(L^2\) · Product of multiplication operators · Almost everywhere bound for a multiplication operator · Bound for a multiplication operator on the support of a vector

DefinitionMultiplication operator on \(L^2\)#✓fully proved

Let \(\mu\) be a measure on a measurable space \(\alpha\) and let \(\varphi \colon \alpha \to \mathbb{C}\) be an essentially bounded, almost everywhere strongly measurable function. The multiplication operator \(M_\varphi\) is the continuous \(\mathbb{C}\)-linear operator on \(L^2(\mu)\) that sends \(f\) to the class of the pointwise product \(x \mapsto \varphi(x) f(x)\).

MathlibExt.Analysis.FunctionalAnalysis.LpMultiplicationOperator.lpMulCLM · 51 lines

noncomputable def lpMulCLM (φ : α → ℂ) (hφ : MemLp φ ∞ μ) :
    Lp ℂ 2 μ →L[ℂ] Lp ℂ 2 μ :=
  LinearMap.mkContinuous
    { toFun := fun f => (memLp_mul_of_memLp_top hφ f).toLp (fun x => φ x * f x)
      map_add' := by
        intro f g
        apply Lp.ext
        calc ⇑((memLp_mul_of_memLp_top hφ (f + g)).toLp (fun x => φ x * (f + g) x))
            =ᵐ[μ] fun x => φ x * (f + g) x := MemLp.coeFn_toLp _
          _ =ᵐ[μ] fun x => φ x * (f x + g x) := by
              filter_upwards [Lp.coeFn_add f g] with x hx
              rw [hx, Pi.add_apply]
          _ =ᵐ[μ] fun x => φ x * f x + φ x * g x :=
            Filter.Eventually.of_forall fun x => mul_add _ _ _
          _ =ᵐ[μ] ⇑((memLp_mul_of_memLp_top hφ f).toLp (fun x => φ x * f x) +
              (memLp_mul_of_memLp_top hφ g).toLp (fun x => φ x * g x)) :=
              (Lp.coeFn_add _ _).trans
                ((MemLp.coeFn_toLp _).add (MemLp.coeFn_toLp _)) |>.symm
      map_smul' := by
        intro c f
        apply Lp.ext
        calc ⇑((memLp_mul_of_memLp_top hφ (c • f)).toLp (fun x => φ x * (c • f) x))
            =ᵐ[μ] fun x => φ x * (c • f) x := MemLp.coeFn_toLp _
          _ =ᵐ[μ] fun x => φ x * (c * f x) := by
              filter_upwards [Lp.coeFn_smul c f] with x hx
              rw [hx, Pi.smul_apply, smul_eq_mul]
          _ =ᵐ[μ] fun x => c * (φ x * f x) :=
            Filter.Eventually.of_forall fun x => by ring
          _ =ᵐ[μ] ⇑(c • (memLp_mul_of_memLp_top hφ f).toLp (fun x => φ x * f x)) :=
              (Lp.coeFn_smul c _).trans (by
                filter_upwards [MemLp.coeFn_toLp (memLp_mul_of_memLp_top hφ f)] with x hx
                simp only [Pi.smul_apply, smul_eq_mul, hx]) |>.symm }
    (eLpNorm φ ∞ μ).toReal
    (by
      intro f
      show ‖(memLp_mul_of_memLp_top hφ f).toLp (fun x => φ x * f x)‖ ≤
        (eLpNorm φ ∞ μ).toReal * ‖f‖
      have hle : eLpNorm (fun x => φ x * f x) 2 μ ≤
          eLpNorm φ ∞ μ * eLpNorm (f : α → ℂ) 2 μ := by
        have h := eLpNorm_le_eLpNorm_top_mul_eLpNorm (2 : ℝ≥0∞) (fun a b => a * b) 1
          (continuous_fst.mul continuous_snd :
      Continuous (Function.uncurry fun a b : ℂ => a * b)) hφ.aestronglyMeasurable (f := φ)
          (g := (f : α → ℂ)) (by filter_upwards with x; simp [nnnorm_mul])
        simpa using h
      rw [Lp.norm_toLp]
      calc (eLpNorm (fun x => φ x * f x) 2 μ).toReal
          ≤ (eLpNorm φ ∞ μ * eLpNorm (f : α → ℂ) 2 μ).toReal :=
            ENNReal.toReal_mono
              (ENNReal.mul_ne_top hφ.eLpNorm_ne_top (Lp.eLpNorm_ne_top f)) hle
        _ = (eLpNorm φ ∞ μ).toReal * ‖f‖ := by
            rw [ENNReal.toReal_mul, Lp.norm_def])

Uses 1 · Used by 15

Statement usesAn essentially bounded multiple of an \(L^2\) function is in \(L^2\)

Used byShifting a multiplication operator by a scalar · Eigenvalues of a multiplication operator on \(L^2\) · Eigenvalues of a multiplication operator on \(L^2\), measurable multiplier · Lower bound for the norm of a multiplication operator · Multiplication operators with almost everywhere equal multipliers coincide · Multiplication by a constant function on \(L^2\) · Product of multiplication operators · Multiplication by one is the identity · Norm of a multiplication operator on L² · Almost everywhere bound for a multiplication operator · Bound for a multiplication operator on the support of a vector · Norm bound for multiplication operators on L² · Norm of an L² multiplication operator with measurable multiplier · Spectrum of a multiplication operator on L² · Spectrum of an L² multiplication operator with measurable multiplier

TheoremMultiplication operators with almost everywhere equal multipliers coincide#✓fully proved

Let \(\mu\) be a measure on a measurable space \(\alpha\) and let \(\varphi, \psi \colon \alpha \to \mathbb{C}\) be essentially bounded, almost everywhere strongly measurable functions. If \(\varphi = \psi\) \(\mu\)-almost everywhere, then the multiplication operators \(M_\varphi\) and \(M_\psi\) on \(L^2(\mu)\) are equal.

theorem lpMulCLM_congr_ae {φ ψ : α → ℂ} (h : φ =ᵐ[μ] ψ) (hφ : MemLp φ ∞ μ)
    (hψ : MemLp ψ ∞ μ) : lpMulCLM φ hφ = lpMulCLM ψ hψ

Uses 2 · Used by 4

Statement usesMultiplication operator on \(L^2\)

Proof usesAn essentially bounded multiple of an \(L^2\) function is in \(L^2\)

Used byEigenvalues of a multiplication operator on \(L^2\) · Norm of a multiplication operator on L² · Spectrum of a multiplication operator on L² · Spectrum of an L² multiplication operator with measurable multiplier

TheoremMultiplication by a constant function on \(L^2\)#✓fully proved

Let \(\mu\) be a measure on a measurable space \(\alpha\) and let \(c \in \mathbb{C}\). The multiplication operator on \(L^2(\mu)\) by the constant function \(x \mapsto c\) sends every \(f \in L^2(\mu)\) to the scalar multiple \(c f\).

theorem lpMulCLM_const_apply (c : ℂ) (f : Lp ℂ 2 μ) :
    lpMulCLM (fun _ => c) (memLp_top_const c) f = c • f

Uses 2 · Used by 1

Statement usesMultiplication operator on \(L^2\)

Proof usesAn essentially bounded multiple of an \(L^2\) function is in \(L^2\)

Used byMultiplication by one is the identity

TheoremMultiplication by one is the identity#✓fully proved

Let \(\mu\) be a measure on a measurable space \(\alpha\). The multiplication operator on \(L^2(\mu)\) by the constant function \(1\) is the identity operator.

theorem lpMulCLM_one : lpMulCLM (fun _ : α => (1 : ℂ)) (memLp_top_const (1 : ℂ))
    = (1 : Lp ℂ 2 μ →L[ℂ] Lp ℂ 2 μ)

Uses 2 · Used by 1

Statement usesMultiplication operator on \(L^2\)

Proof usesMultiplication by a constant function on \(L^2\)

Used bySpectrum of an L² multiplication operator with measurable multiplier

TheoremProduct of multiplication operators#✓fully proved

Let \(\mu\) be a measure on a measurable space \(\alpha\) and, for an essentially bounded, almost everywhere strongly measurable function \(\chi \colon \alpha \to \mathbb{C}\), let \(M_\chi\) be the multiplication operator \(f \mapsto \chi f\) on \(L^2(\mu)\). Let \(\varphi, \psi \colon \alpha \to \mathbb{C}\) be essentially bounded, almost everywhere strongly measurable functions such that the pointwise product \(\varphi\psi \colon x \mapsto \varphi(x)\psi(x)\) is also essentially bounded and almost everywhere strongly measurable. Then \(M_{\varphi\psi} = M_\varphi M_\psi\), where the right side is the composition of operators.

theorem lpMulCLM_mul {φ ψ : α → ℂ} (hφ : MemLp φ ∞ μ) (hψ : MemLp ψ ∞ μ)
    (hφψ : MemLp (fun x => φ x * ψ x) ∞ μ) :
    lpMulCLM (fun x => φ x * ψ x) hφψ = lpMulCLM φ hφ * lpMulCLM ψ hψ

Uses 2 · Used by 1

Statement usesMultiplication operator on \(L^2\)

Proof usesAn essentially bounded multiple of an \(L^2\) function is in \(L^2\)

Used bySpectrum of an L² multiplication operator with measurable multiplier

TheoremShifting a multiplication operator by a scalar#✓fully proved

Let \(\mu\) be a measure on a measurable space \(\alpha\), let \(\varphi : \alpha \to \mathbb{C}\) be in \(L^\infty(\mu)\), let \(z \in \mathbb{C}\), and suppose the function \(x \mapsto z - \varphi(x)\) is also in \(L^\infty(\mu)\). For \(\psi \in L^\infty(\mu)\) write \(M_\psi\) for the multiplication operator \(f \mapsto \psi f\) on \(L^2(\mu)\). Then \(z I - M_\varphi = M_{z - \varphi}\), where \(I\) is the identity operator on \(L^2(\mu)\).

theorem algebraMap_sub_lpMulCLM {φ : α → ℂ} (hφ : MemLp φ ∞ μ) (z : ℂ)
    (h : MemLp (fun x => z - φ x) ∞ μ) :
    algebraMap ℂ (Lp ℂ 2 μ →L[ℂ] Lp ℂ 2 μ) z - lpMulCLM φ hφ =
      lpMulCLM (fun x => z - φ x) h

Uses 2 · Used by 1

Statement usesMultiplication operator on \(L^2\)

Proof usesAn essentially bounded multiple of an \(L^2\) function is in \(L^2\)

Used bySpectrum of an L² multiplication operator with measurable multiplier

TheoremMeasurable representatives of essentially bounded functions#✓fully proved

Let \(\mu\) be a measure on a measurable space \(\alpha\) and let \(\varphi : \alpha \to \mathbb{C}\) be in \(L^\infty(\mu)\), that is, \(\mu\)-almost everywhere strongly measurable and essentially bounded. Then there is a measurable \(\psi : \alpha \to \mathbb{C}\) such that \(\varphi = \psi\) \(\mu\)-almost everywhere and \(\psi\) is in \(L^\infty(\mu)\).

In particular \(\varphi\) and \(\psi\) define the same multiplication operator on \(L^2(\mu)\).

theorem exists_measurable_memLp {φ : α → ℂ} (hφ : MemLp φ ∞ μ) :
    ∃ ψ : α → ℂ, Measurable ψ ∧ φ =ᵐ[μ] ψ ∧ MemLp ψ ∞ μ

Used by 3

Used byEigenvalues of a multiplication operator on \(L^2\) · Norm of a multiplication operator on L² · Spectrum of a multiplication operator on L²

TheoremPointwise bound by the essential supremum norm#✓fully proved

Let \(\mu\) be a measure on a measurable space \(\alpha\) and let \(\varphi : \alpha \to \mathbb{C}\) be in \(L^\infty(\mu)\), that is, \(\mu\)-almost everywhere strongly measurable and essentially bounded. Then \(|\varphi(x)| \le \|\varphi\|_{L^\infty(\mu)}\) for \(\mu\)-almost every \(x \in \alpha\).

theorem ae_norm_le_eLpNorm_top {φ : α → ℂ} (hφ : MemLp φ ∞ μ) :
    ∀ᵐ x ∂μ, ‖φ x‖ ≤ (eLpNorm φ ∞ μ).toReal

Used by 1

Used byNorm bound for multiplication operators on L²

TheoremAlmost everywhere bound for a multiplication operator#✓fully proved

Let \(\mu\) be a measure on a measurable space \(\alpha\), let \(\varphi \colon \alpha \to \mathbb{C}\) be an essentially bounded, almost everywhere strongly measurable function, and let \(M_\varphi\) be the multiplication operator on \(L^2(\mu)\). If \(C\) is a real number with \(|\varphi(x)| \le C\) for \(\mu\)-almost every \(x\), then \(\|M_\varphi f\| \le C \|f\|\) for every \(f \in L^2(\mu)\).

theorem norm_lpMulCLM_apply_le_of_ae_bound {φ : α → ℂ} (hφ : MemLp φ ∞ μ) {C : ℝ}
    (f : Lp ℂ 2 μ) (hC : ∀ᵐ x ∂μ, ‖φ x‖ ≤ C) :
    ‖lpMulCLM φ hφ f‖ ≤ C * ‖f‖

Uses 2 · Used by 1

Statement usesMultiplication operator on \(L^2\)

Proof usesAn essentially bounded multiple of an \(L^2\) function is in \(L^2\)

Used byNorm bound for multiplication operators on L²

TheoremBound for a multiplication operator on the support of a vector#✓fully proved

Let \(\mu\) be a measure on a measurable space \(\alpha\), let \(\varphi \colon \alpha \to \mathbb{C}\) be an essentially bounded, almost everywhere strongly measurable function, and let \(M_\varphi\) be the multiplication operator on \(L^2(\mu)\). If \(C\) is a real number and \(f \in L^2(\mu)\) is such that, for \(\mu\)-almost every \(x\), either \(|\varphi(x)| \le C\) or \(f(x) = 0\), then \(\|M_\varphi f\| \le C \|f\|\).

theorem norm_lpMulCLM_apply_le_of_ae_support {φ : α → ℂ} (hφ : MemLp φ ∞ μ) {C : ℝ}
    (f : Lp ℂ 2 μ) (hC : ∀ᵐ x ∂μ, ‖φ x‖ ≤ C ∨ f x = 0) :
    ‖lpMulCLM φ hφ f‖ ≤ C * ‖f‖

Uses 2 · Used by 1

Statement usesMultiplication operator on \(L^2\)

Proof usesAn essentially bounded multiple of an \(L^2\) function is in \(L^2\)

Used bySpectrum of an L² multiplication operator with measurable multiplier

TheoremLower bound for the norm of a multiplication operator#✓fully proved

Let \(\mu\) be a measure on a measurable space \(\alpha\), let \(\varphi \colon \alpha \to \mathbb{C}\) be an essentially bounded, almost everywhere strongly measurable function, and let \(M_\varphi\) be the multiplication operator \(f \mapsto \varphi f\) on \(L^2(\mu)\). If \(C \ge 0\) is a real number and \(f \in L^2(\mu)\) satisfies \(\|f\| = 1\) and \(C\,|f(x)| \le |\varphi(x)|\,|f(x)|\) for \(\mu\)-almost every \(x\), then \(C \le \|M_\varphi\|\).

theorem le_norm_lpMulCLM_of_ae_le {φ : α → ℂ} (hφ : MemLp φ ∞ μ) {C : ℝ}
    (hC0 : 0 ≤ C) {f : Lp ℂ 2 μ} (hf : ‖f‖ = 1)
    (h : ∀ᵐ x ∂μ, C * ‖f x‖ ≤ ‖φ x‖ * ‖f x‖) : C ≤ ‖lpMulCLM φ hφ‖

Uses 2 · Used by 1

Statement usesMultiplication operator on \(L^2\)

Proof usesAn essentially bounded multiple of an \(L^2\) function is in \(L^2\)

Used byNorm of an L² multiplication operator with measurable multiplier

TheoremNorm bound for multiplication operators on L²#✓fully proved

Let \(\mu\) be a measure on a measurable space \(\alpha\) and let \(\varphi : \alpha \to \mathbb{C}\) be in \(L^\infty(\mu)\), with essential supremum norm \(\|\varphi\|_\infty\). Then the multiplication operator \(M_\varphi\) on the complex space \(L^2(\mu)\) has operator norm \(\|M_\varphi\| \le \|\varphi\|_\infty\).

theorem norm_lpMulCLM_le {φ : α → ℂ} (hφ : MemLp φ ∞ μ) :
    ‖lpMulCLM φ hφ‖ ≤ (eLpNorm φ ∞ μ).toReal

Uses 3 · Used by 1

Statement usesMultiplication operator on \(L^2\)

Proof usesPointwise bound by the essential supremum norm · Almost everywhere bound for a multiplication operator

Used byNorm of an L² multiplication operator with measurable multiplier

TheoremNormalized indicator of a set of finite positive measure#✓fully proved

Let \(\mu\) be a measure on a measurable space \(\alpha\) and let \(t \subseteq \alpha\) be a measurable set with \(0 < \mu(t) < \infty\). Then there is \(u \in L^2(\mu)\) (complex valued) with \(\|u\| = 1\) such that \(u(x) = \mu(t)^{-1/2}\) for \(\mu\)-almost every \(x \in t\) and \(u(x) = 0\) for \(\mu\)-almost every \(x \notin t\).

theorem exists_unit_vector {t : Set α} (ht : MeasurableSet t) (hμt : μ t ≠ ∞)
    (hpos : 0 < μ t) :
    ∃ u : Lp ℂ 2 μ, ‖u‖ = 1 ∧
      (∀ᵐ x ∂μ, x ∈ t → u x = (RCLike.ofReal ((μ t).toReal ^ (-1 / 2 : ℝ)) : ℂ)) ∧
      (∀ᵐ x ∂μ, x ∉ t → u x = 0)

Used by 3

Used byEigenvalues of a multiplication operator on \(L^2\), measurable multiplier · Norm of an L² multiplication operator with measurable multiplier · Spectrum of an L² multiplication operator with measurable multiplier

TheoremNorm of an L² multiplication operator with measurable multiplier#✓fully proved

Let \(\mu\) be a \(\sigma\)-finite measure on a measurable space \(\alpha\) and let \(\varphi : \alpha \to \mathbb{C}\) be a measurable function in \(L^\infty(\mu)\), with essential supremum norm \(\|\varphi\|_\infty\). Then the multiplication operator \(M_\varphi\) on the complex space \(L^2(\mu)\) has operator norm \(\|M_\varphi\| = \|\varphi\|_\infty\).

theorem norm_lpMulCLM_of_measurable {φ : α → ℂ} (hφ : MemLp φ ∞ μ)
    (hφm : Measurable φ) : ‖lpMulCLM φ hφ‖ = (eLpNorm φ ∞ μ).toReal

Uses 4 · Used by 1

Statement usesMultiplication operator on \(L^2\)

Proof usesNormalized indicator of a set of finite positive measure · Lower bound for the norm of a multiplication operator · Norm bound for multiplication operators on L²

Used byNorm of a multiplication operator on L²

TheoremNorm of a multiplication operator on L²#✓fully proved

Let \(\mu\) be a \(\sigma\)-finite measure on a measurable space \(\alpha\) and let \(\varphi : \alpha \to \mathbb{C}\) be in \(L^\infty(\mu)\), with essential supremum norm \(\|\varphi\|_\infty\). Then the multiplication operator \(M_\varphi\) on the complex space \(L^2(\mu)\) has operator norm \(\|M_\varphi\| = \|\varphi\|_\infty\).

theorem norm_lpMulCLM {φ : α → ℂ} (hφ : MemLp φ ∞ μ) :
    ‖lpMulCLM φ hφ‖ = (eLpNorm φ ∞ μ).toReal

Uses 4

Statement usesMultiplication operator on \(L^2\)

Proof usesMeasurable representatives of essentially bounded functions · Multiplication operators with almost everywhere equal multipliers coincide · Norm of an L² multiplication operator with measurable multiplier

TheoremSpectrum of an L² multiplication operator with measurable multiplier#✓fully proved

Let \(\mu\) be a \(\sigma\)-finite measure on a measurable space \(\alpha\) and let \(\varphi : \alpha \to \mathbb{C}\) be a measurable function in \(L^\infty(\mu)\). Then the spectrum of the multiplication operator \(M_\varphi\), as an element of the complex algebra of bounded operators on \(L^2(\mu)\), equals the essential range of \(\varphi\) with respect to \(\mu\).

theorem spectrum_lpMulCLM_of_measurable {φ : α → ℂ} (hφ : MemLp φ ∞ μ)
    (hφm : Measurable φ) : spectrum ℂ (lpMulCLM φ hφ) = essentialRange φ μ

Uses 9 · Used by 1

Statement usesEssential range · Multiplication operator on \(L^2\)

Proof usesShifting a multiplication operator by a scalar · Normalized indicator of a set of finite positive measure · Multiplication operators with almost everywhere equal multipliers coincide · Product of multiplication operators · Multiplication by one is the identity · Bound for a multiplication operator on the support of a vector · Points outside the essential range

Used bySpectrum of a multiplication operator on L²

TheoremSpectrum of a multiplication operator on L²#✓fully proved

Let \(\mu\) be a \(\sigma\)-finite measure on a measurable space \(\alpha\) and let \(\varphi : \alpha \to \mathbb{C}\) be in \(L^\infty(\mu)\). Then the spectrum of the multiplication operator \(M_\varphi\), as an element of the complex algebra of bounded operators on \(L^2(\mu)\), equals the essential range of \(\varphi\) with respect to \(\mu\).

theorem spectrum_lpMulCLM {φ : α → ℂ} (hφ : MemLp φ ∞ μ) :
    spectrum ℂ (lpMulCLM φ hφ) = essentialRange φ μ

Uses 6

Statement usesEssential range · Multiplication operator on \(L^2\)

Proof usesThe essential range is invariant under almost-everywhere equality · Measurable representatives of essentially bounded functions · Multiplication operators with almost everywhere equal multipliers coincide · Spectrum of an L² multiplication operator with measurable multiplier

TheoremEigenvalues of a multiplication operator on \(L^2\), measurable multiplier#✓fully proved

Let \(\mu\) be a \(\sigma\)-finite measure on a measurable space \(\alpha\), let \(\varphi : \alpha \to \mathbb{C}\) be measurable and in \(L^\infty(\mu)\), and let \(M_\varphi\) be the multiplication operator \(f \mapsto \varphi f\) on \(L^2(\mu)\). Then \(z \in \mathbb{C}\) is an eigenvalue of \(M_\varphi\) if and only if \(\mu(\{x \in \alpha : \varphi(x) = z\}) > 0\).

theorem hasEigenvalue_lpMulCLM_iff_of_measurable {φ : α → ℂ} (hφ : MemLp φ ∞ μ)
    (hφm : Measurable φ) (z : ℂ) :
    Module.End.HasEigenvalue (lpMulCLM φ hφ : Lp ℂ 2 μ →ₗ[ℂ] Lp ℂ 2 μ) z ↔
      0 < μ {x | φ x = z}

Uses 3 · Used by 1

Statement usesMultiplication operator on \(L^2\)

Proof usesNormalized indicator of a set of finite positive measure · An essentially bounded multiple of an \(L^2\) function is in \(L^2\)

Used byEigenvalues of a multiplication operator on \(L^2\)

TheoremEigenvalues of a multiplication operator on \(L^2\)#✓fully proved

Let \(\mu\) be a \(\sigma\)-finite measure on a measurable space \(\alpha\), let \(\varphi : \alpha \to \mathbb{C}\) be in \(L^\infty(\mu)\), and let \(M_\varphi\) be the multiplication operator \(f \mapsto \varphi f\) on \(L^2(\mu)\). Then \(z \in \mathbb{C}\) is an eigenvalue of \(M_\varphi\) if and only if \(\mu(\{x \in \alpha : \varphi(x) = z\}) > 0\).

theorem hasEigenvalue_lpMulCLM_iff {φ : α → ℂ} (hφ : MemLp φ ∞ μ) (z : ℂ) :
    Module.End.HasEigenvalue (lpMulCLM φ hφ : Lp ℂ 2 μ →ₗ[ℂ] Lp ℂ 2 μ) z ↔
      0 < μ {x | φ x = z}

Uses 4

Statement usesMultiplication operator on \(L^2\)

Proof usesMeasurable representatives of essentially bounded functions · Eigenvalues of a multiplication operator on \(L^2\), measurable multiplier · Multiplication operators with almost everywhere equal multipliers coincide

AbbreviationThe space \(L^2((1,2))\)#✓fully proved

\(L^2([1,2])\) is the space of real-valued functions on \(\mathbb{R}\) that are square-integrable for Lebesgue measure restricted to \([1,2]\), taken modulo equality almost everywhere on \([1,2]\).

noncomputable abbrev L2OnOneTwo : Type :=
  (ℝ →₂[volume.restrict (Set.Icc (1 : ℝ) 2)] ℝ)

Used by 1

Used byMultiplication by \(x\) on \(L^2((1,2))\) is bounded, bijective and self-adjoint

TheoremMultiplication by \(x\) on \(L^2((1,2))\) is bounded, bijective and self-adjoint#●ready to prove

Let \(L^2([1,2])\) be the real Hilbert space of square-integrable real functions for Lebesgue measure on \([1,2]\), with inner product \(\langle f, g\rangle = \int_1^2 f(x)g(x)\,dx\). Let \(T : L^2([1,2]) \to L^2([1,2])\) be a linear map such that for every \(f\), \((Tf)(x) = x f(x)\) for almost every \(x \in [1,2]\). Then \(T\) is continuous and bijective, and \(T = T^*\), where \(T^*\) is the Hilbert space adjoint of \(T\).

public theorem_wanted continuous_bijective_selfAdjoint_of_mul_id_L2_Icc_one_two
    (T : L2OnOneTwo →ₗ[ℝ] L2OnOneTwo)
    (hT : ∀ f : L2OnOneTwo,
      T f =ᵐ[volume.restrict (Set.Icc (1 : ℝ) 2)] fun x : ℝ => x * f x) :
    Continuous T ∧ Function.Bijective T ∧
      ∃ Tc : L2OnOneTwo →L[ℝ] L2OnOneTwo,
        Tc.toLinearMap = T ∧ Tc.adjoint = Tc

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Operator theory; General theory of linear operators), problem ma_proofbench_l2_26.

Uses 1

Statement usesThe space \(L^2((1,2))\)

TheoremMultiplication by \(t\) is bounded on \(L^2((0,1))\)#●ready to prove

Let \(L^2([0,1])\) be the space of real square-integrable functions for Lebesgue measure on \([0,1]\). There is a bounded linear operator \(T : L^2([0,1]) \to L^2([0,1])\) such that for every \(f \in L^2([0,1])\), \((Tf)(t) = t f(t)\) for almost every \(t \in [0,1]\).

public theorem_wanted exists_continuousLinearMap_mul_id_L2_Icc :
    ∃ T : Lp ℝ 2 (volume.restrict (Set.Icc (0 : ℝ) 1)) →L[ℝ]
        Lp ℝ 2 (volume.restrict (Set.Icc (0 : ℝ) 1)),
      ∀ f : Lp ℝ 2 (volume.restrict (Set.Icc (0 : ℝ) 1)),
        ((T f : Lp ℝ 2 (volume.restrict (Set.Icc (0 : ℝ) 1))) : ℝ → ℝ)
          =ᵐ[volume.restrict (Set.Icc (0 : ℝ) 1)]
            fun t => t * (f : ℝ → ℝ) t

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Operator theory; General theory of linear operators), problem ma_proofbench_l1_31.

26 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.