Source indexedlemma · leanprover/lean4:v4.33.0-rc1

ProbabilityTheory.identDistrib_of_finiteRange

PFR.ForMathlib.FiniteRange.IdentDistrib · PFR/ForMathlib/FiniteRange/IdentDistrib.lean:24 to 46

Source documentation

If X has identical distribution to X₀, and X₀ has finite range, then X is almost everywhere equivalent to a random variable of finite range.

Exact Lean statement

lemma identDistrib_of_finiteRange {Ω Ω₀ S : Type*}
    [MeasurableSpace Ω] [MeasurableSpace Ω₀] [MeasurableSpace S] [MeasurableSingletonClass S]
    [hS : Nonempty S] {μ : Measure Ω} {μ₀ : Measure Ω₀} {X₀ : Ω₀ → S} [FiniteRange X₀] {X : Ω → S}
    (hX : Measurable X) (hi : IdentDistrib X₀ X μ₀ μ) :
    ∃ X' : Ω → S, Measurable X' ∧ FiniteRange X' ∧ X' =ᵐ[μ] X

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma identDistrib_of_finiteRange {Ω Ω₀ S : Type*}    [MeasurableSpace Ω] [MeasurableSpace Ω₀] [MeasurableSpace S] [MeasurableSingletonClass S]    [hS : Nonempty S] {μ : Measure Ω} {μ₀ : Measure Ω₀} {X₀ : Ω₀ → S} [FiniteRange X₀] {X : Ω → S}    (hX : Measurable X) (hi : IdentDistrib X₀ X μ₀ μ) :    ∃ X' : Ω → S, Measurable X' ∧ FiniteRange X' ∧ X' =ᵐ[μ] X := by  set A := FiniteRange.toFinset X₀  classical  let X' (ω : Ω) : S := if (X ω ∈ A) then X ω else hS.some  refine ⟨X', ?_, ?_, ?_⟩  · exact .ite (.preimage (Finset.measurableSet A) hX) hX measurable_const  · apply finiteRange_of_finset X' (A ∪ {hS.some})    intro ω    simp [X']    split <;> simp [*]  apply Filter.eventuallyEq_of_mem (s := X ⁻¹' A)  · rw [mem_ae_iff, ← Set.preimage_compl, ← IdentDistrib.measure_preimage_eq hi]    · convert measure_empty (μ := μ₀)      ext ω      simp [A]    measurability  intro ω  simp only [mem_preimage, Finset.mem_coe, ite_eq_left_iff, X']  tauto