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

ProbabilityTheory.independent_copies_finiteRange

PFR.ForMathlib.FiniteRange.IdentDistrib · PFR/ForMathlib/FiniteRange/IdentDistrib.lean:50 to 69

Source documentation

A version of independent_copies that guarantees that the copies have FiniteRange if the original variables do.

Exact Lean statement

lemma independent_copies_finiteRange {X : Ω → α} {Y : Ω' → β}
    (hX : Measurable X) (hY : Measurable Y) [FiniteRange X] [FiniteRange Y]
    [MeasurableSingletonClass α] [MeasurableSingletonClass β]
    (μ : Measure Ω) (μ' : Measure Ω') [IsProbabilityMeasure μ] [IsProbabilityMeasure μ'] :
    ∃ ν : Measure (α × β), ∃ X' : α × β → α, ∃
    Y' : α × β → β, IsProbabilityMeasure ν
      ∧ Measurable X' ∧ Measurable Y' ∧ IndepFun X' Y' ν
      ∧ IdentDistrib X' X ν μ ∧ IdentDistrib Y' Y ν μ' ∧ FiniteRange X' ∧ FiniteRange Y'

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma independent_copies_finiteRange {X : Ω → α} {Y : Ω' → β}    (hX : Measurable X) (hY : Measurable Y) [FiniteRange X] [FiniteRange Y]    [MeasurableSingletonClass α] [MeasurableSingletonClass β]    (μ : Measure Ω) (μ' : Measure Ω') [IsProbabilityMeasure μ] [IsProbabilityMeasure μ'] :    ∃ ν : Measure (α × β), ∃ X' : α × β → α, ∃    Y' : α × β → β, IsProbabilityMeasure ν      ∧ Measurable X' ∧ Measurable Y' ∧ IndepFun X' Y' ν      ∧ IdentDistrib X' X ν μ ∧ IdentDistrib Y' Y ν μ' ∧ FiniteRange X' ∧ FiniteRange Y' := by  have : Nonempty α := μ.nonempty_of_neZero.map X  have : Nonempty β := μ'.nonempty_of_neZero.map Y  obtain ⟨ν, X', Y', hν, hX', hY', hind, hIdX, hIdY⟩ := independent_copies hX hY μ μ'  rcases identDistrib_of_finiteRange hX' hIdX.symm with ⟨X'', hX'', hX''_finite, hX''_eq⟩  rcases identDistrib_of_finiteRange hY' hIdY.symm with ⟨Y'', hY'', hY''_finite, hY''_eq⟩  use ν, X'', Y''  refine ⟨hν, hX'', hY'', ?_, ?_, ?_, hX''_finite, hY''_finite⟩  · exact hind.congr hX''_eq.symm hY''_eq.symm  · convert IdentDistrib.trans _ hIdX    exact IdentDistrib.of_ae_eq (Measurable.aemeasurable hX'') hX''_eq  · convert IdentDistrib.trans _ hIdY    exact IdentDistrib.of_ae_eq (Measurable.aemeasurable hY'') hY''_eq