`BookProof.ChapterMeasureAtomicDiffuse.exists_atomic_diffuse_decomposition` [IsFiniteMeasure mu] : ∃ (A : Set α) (mua mud : Measure α), A.Countable ∧ MeasurableSet A ∧ mu = mua + m

Proved

BookProof.ChapterMeasureAtomicDiffuse.exists_atomic_diffuse_decomposition

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterMeasureAtomicDiffuse.

BookProof.ChapterMeasureAtomicDiffuse.exists_atomic_diffuse_decomposition [IsFiniteMeasure mu] : ∃ (A : Set α) (mua mud : Measure α), A.Countable ∧ MeasurableSet A ∧ mu = mua + mud ∧ mua = Measure.sum (fun x : A => mu {(x : α)} • Measure.dirac (x : α)) ∧ mua Aᶜ = 0 ∧ NullSingletonClass mud

Formalization note: Lean 4 identifier BookProof.ChapterMeasureAtomicDiffuse.exists_atomic_diffuse_decomposition.

Preamble

-- Generated from ChapterMeasureAtomicDiffuse.lean — theorem BookProof.ChapterMeasureAtomicDiffuse.exists_atomic_diffuse_decomposition
import Mathlib
import Definitions.Def_ChapterMeasureAtomicDiffuse
open BookProof.ChapterMeasureAtomicDiffuse


noncomputable section

open MeasureTheory Complex



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

Formal statement

theorem BookProof.ChapterMeasureAtomicDiffuse.exists_atomic_diffuse_decomposition [IsFiniteMeasure mu] :
    ∃ (A : Set α) (mua mud : Measure α), A.Countable ∧ MeasurableSet A ∧
      mu = mua + mud ∧
      mua = Measure.sum (fun x : A => mu {(x : α)} • Measure.dirac (x : α)) ∧
      mua Aᶜ = 0 ∧ NullSingletonClass mud := by sorry

View graph