`BookProof.ChapterLpScaleMeasure.normalized_multiplication_model` [IsFiniteMeasure nu] (hne : nu Set.univ ≠ 0) : ∃ U : Lp ℂ 2 ((nu Set.univ)⁻¹ • nu) ≃ₗᵢ[ℂ] Lp ℂ 2 nu, ∀ (g...

Proved

BookProof.ChapterLpScaleMeasure.normalized_multiplication_model

by leonardopedro · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterLpScaleMeasure.

BookProof.ChapterLpScaleMeasure.normalized_multiplication_model [IsFiniteMeasure nu] (hne : nu Set.univ ≠ 0) : ∃ U : Lp ℂ 2 ((nu Set.univ)⁻¹ • nu) ≃ₗᵢ[ℂ] Lp ℂ 2 nu, ∀ (g : α → ℂ) (hg : MemLp g ⊤ ((nu Set.univ)⁻¹ • nu)) (u : Lp ℂ 2 ((nu Set.univ)⁻¹ • nu)), (U (multOp g hg u) : α → ℂ) =ᵐ[nu] fun x => g x * (U u : α → ℂ) x

Formalization note: Lean 4 identifier BookProof.ChapterLpScaleMeasure.normalized_multiplication_model.

Preamble

-- Generated from ChapterLpScaleMeasure.lean — theorem BookProof.ChapterLpScaleMeasure.normalized_multiplication_model
import Mathlib
import Definitions.Def_ChapterLpScaleMeasure
import Definitions.Def_ChapterLinftyMultiplication
open BookProof.ChapterLinftyMultiplication
open BookProof.ChapterLpScaleMeasure


noncomputable section

open MeasureTheory ENNReal


open BookProof.ChapterLinftyMultiplication

variable {α : Type*} [MeasurableSpace α] {nu : Measure α} {c : ENNReal}

Formal statement

theorem BookProof.ChapterLpScaleMeasure.normalized_multiplication_model [IsFiniteMeasure nu] (hne : nu Set.univ ≠ 0) :
    ∃ U : Lp ℂ 2 ((nu Set.univ)⁻¹ • nu) ≃ₗᵢ[ℂ] Lp ℂ 2 nu,
      ∀ (g : α → ℂ) (hg : MemLp g ⊤ ((nu Set.univ)⁻¹ • nu))
        (u : Lp ℂ 2 ((nu Set.univ)⁻¹ • nu)),
        (U (multOp g hg u) : α → ℂ) =ᵐ[nu] fun x => g x * (U u : α → ℂ) x := by sorry

View graph