`BookProof.ChapterMeasurementLLN.outcomeIndicator_integral` (M : ℕ → Ω → Fin k) (a : Fin k) (hM : Measurable (M 0)) : ∫ ω, outcomeIndicator M a 0 ω ∂μ = (μ {ω | M 0 ω = a}).toReal

Proved

BookProof.ChapterMeasurementLLN.outcomeIndicator_integral

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterMeasurementLLN.

BookProof.ChapterMeasurementLLN.outcomeIndicator_integral (M : ℕ → Ω → Fin k) (a : Fin k) (hM : Measurable (M 0)) : ∫ ω, outcomeIndicator M a 0 ω ∂μ = (μ {ω | M 0 ω = a}).toReal

Formalization note: Lean 4 identifier BookProof.ChapterMeasurementLLN.outcomeIndicator_integral.

Preamble

-- Generated from ChapterMeasurementLLN.lean — theorem BookProof.ChapterMeasurementLLN.outcomeIndicator_integral
import Mathlib
import Definitions.Def_ChapterMeasurementLLN
open BookProof.ChapterMeasurementLLN


open MeasureTheory ProbabilityTheory
open scoped ENNReal


variable {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
variable {k : ℕ}

Formal statement

theorem BookProof.ChapterMeasurementLLN.outcomeIndicator_integral (M : ℕ → Ω → Fin k) (a : Fin k)
    (hM : Measurable (M 0)) :
    ∫ ω, outcomeIndicator M a 0 ω ∂μ = (μ {ω | M 0 ω = a}).toReal := by sorry

View graph