`BookProof.ChapterMeasurementLLN.measurement_frequency_tendsto` (M : ℕ → Ω → Fin k) (a : Fin k) (hmeas : ∀ i, Measurable (M i)) (hindep : Pairwise (fun i j => IndepFun (M i) (M j)

Proved

BookProof.ChapterMeasurementLLN.measurement_frequency_tendsto

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterMeasurementLLN.

BookProof.ChapterMeasurementLLN.measurement_frequency_tendsto (M : ℕ → Ω → Fin k) (a : Fin k) (hmeas : ∀ i, Measurable (M i)) (hindep : Pairwise (fun i j => IndepFun (M i) (M j) μ)) (hident : ∀ i, IdentDistrib (M i) (M 0) μ μ) : ∀ᵐ ω ∂μ, Filter.Tendsto (fun n => (∑ i ∈ Finset.range n, outcomeIndicator M a i ω) / n) Filter.atTop (nhds (μ {ω | M 0 ω = a}).toReal)

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

Preamble

-- Generated from ChapterMeasurementLLN.lean — theorem BookProof.ChapterMeasurementLLN.measurement_frequency_tendsto
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.measurement_frequency_tendsto (M : ℕ → Ω → Fin k) (a : Fin k)
    (hmeas : ∀ i, Measurable (M i))
    (hindep : Pairwise (fun i j => IndepFun (M i) (M j) μ))
    (hident : ∀ i, IdentDistrib (M i) (M 0) μ μ) :
    ∀ᵐ ω ∂μ, Filter.Tendsto
      (fun n => (∑ i ∈ Finset.range n, outcomeIndicator M a i ω) / n)
      Filter.atTop (nhds (μ {ω | M 0 ω = a}).toReal) := by sorry

View graph