`BookProof.ChapterAtomicDiagonalModel.multOp_atomVec` {g : α → ℂ} (hg : MemLp g ⊤ mu) (a : atomSet mu) : multOp g hg (atomVec mu a) = g (a : α) • atomVec mu a

Proved

BookProof.ChapterAtomicDiagonalModel.multOp_atomVec

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterAtomicDiagonalModel.

BookProof.ChapterAtomicDiagonalModel.multOp_atomVec {g : α → ℂ} (hg : MemLp g ⊤ mu) (a : atomSet mu) : multOp g hg (atomVec mu a) = g (a : α) • atomVec mu a

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

Preamble

-- Generated from ChapterAtomicDiagonalModel.lean — theorem BookProof.ChapterAtomicDiagonalModel.multOp_atomVec
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.multOp_atomVec {g : α → ℂ} (hg : MemLp g ⊤ mu) (a : atomSet mu) :
    multOp g hg (atomVec mu a) = g (a : α) • atomVec mu a := by sorry

View graph