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

Proved

BookProof.ChapterMeasurementLLN.measurement_average_tendsto

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterMeasurementLLN.

BookProof.ChapterMeasurementLLN.measurement_average_tendsto (M : ℕ → Ω → Fin k) (f : 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, f (M i ω)) / n) Filter.atTop (nhds (∫ ω, f (M 0 ω) ∂μ))

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

Preamble

-- Generated from ChapterMeasurementLLN.lean — theorem BookProof.ChapterMeasurementLLN.measurement_average_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_average_tendsto (M : ℕ → Ω → Fin k) (f : 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, f (M i ω)) / n)
      Filter.atTop (nhds (∫ ω, f (M 0 ω) ∂μ)) := by sorry

View graph