`BookProof.ChapterAtomicDiagonalModel.atomic_multiplication_model_diagonal` (hpure : mu (atomSet mu)ᶜ = 0) : ∃ B : HilbertBasis (atomSet mu) ℂ (Lp ℂ 2 mu), ∀ (g : α → ℂ) (hg : MemL

Proved

BookProof.ChapterAtomicDiagonalModel.atomic_multiplication_model_diagonal

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterAtomicDiagonalModel.

BookProof.ChapterAtomicDiagonalModel.atomic_multiplication_model_diagonal (hpure : mu (atomSet mu)ᶜ = 0) : ∃ B : HilbertBasis (atomSet mu) ℂ (Lp ℂ 2 mu), ∀ (g : α → ℂ) (hg : MemLp g ⊤ mu) (a : atomSet mu), multOp g hg (B a) = g (a : α) • B a

Formalization note: Lean 4 identifier BookProof.ChapterAtomicDiagonalModel.atomic_multiplication_model_diagonal.

Preamble

-- Generated from ChapterAtomicDiagonalModel.lean — theorem BookProof.ChapterAtomicDiagonalModel.atomic_multiplication_model_diagonal
import Definitions.Def_ChapterMeasureAtomicDiffuse
import Mathlib
import Definitions.Def_ChapterAtomicDiagonalModel
import Definitions.Def_ChapterLinftyMultiplication
open BookProof.ChapterLinftyMultiplication
open BookProof.ChapterAtomicDiagonalModel


noncomputable section

open MeasureTheory


open BookProof.ChapterMeasureAtomicDiffuse BookProof.ChapterLinftyMultiplication

variable {α : Type*} [MeasurableSpace α] [MeasurableSingletonClass α]
  (mu : Measure α) [IsFiniteMeasure mu]

Formal statement

theorem BookProof.ChapterAtomicDiagonalModel.atomic_multiplication_model_diagonal (hpure : mu (atomSet mu)ᶜ = 0) :
    ∃ B : HilbertBasis (atomSet mu) ℂ (Lp ℂ 2 mu),
      ∀ (g : α → ℂ) (hg : MemLp g ⊤ mu) (a : atomSet mu),
        multOp g hg (B a) = g (a : α) • B a := by sorry

View graph