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

ProbabilityTheory.independent_copies3_nondep_finiteRange

PFR.ForMathlib.FiniteRange.IdentDistrib · PFR/ForMathlib/FiniteRange/IdentDistrib.lean:73 to 106

Source documentation

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

Exact Lean statement

lemma independent_copies3_nondep_finiteRange {α : Type u}
    [mS : MeasurableSpace α] [MeasurableSingletonClass α]
    {Ω₁ : Type u_1} {Ω₂ : Type u_2} {Ω₃ : Type u_3}
    [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] [MeasurableSpace Ω₃]
    {X₁ : Ω₁ → α} {X₂ : Ω₂ → α} {X₃ : Ω₃ → α}
    (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hX₃ : Measurable X₃)
    [FiniteRange X₁] [FiniteRange X₂] [FiniteRange X₃]
    (μ₁ : Measure Ω₁) (μ₂ : Measure Ω₂) (μ₃ : Measure Ω₃)
    [hμ₁ : IsProbabilityMeasure μ₁] [hμ₂ : IsProbabilityMeasure μ₂]
    [hμ₃ : IsProbabilityMeasure μ₃] :
    ∃ (A : Type (max u_1 u_2 u_3)) (_ : MeasurableSpace A) (μA : Measure A)
      (X₁' X₂' X₃' : A → α),
    IsProbabilityMeasure μA ∧
    iIndepFun ![X₁', X₂', X₃'] μA ∧
      Measurable X₁' ∧ Measurable X₂' ∧ Measurable X₃' ∧
      IdentDistrib X₁' X₁ μA μ₁ ∧ IdentDistrib X₂' X₂ μA μ₂ ∧ IdentDistrib X₃' X₃ μA μ₃ ∧
      FiniteRange X₁' ∧ FiniteRange X₂' ∧ FiniteRange X₃'

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma independent_copies3_nondep_finiteRange {α : Type u}    [mS : MeasurableSpace α] [MeasurableSingletonClass α]    {Ω₁ : Type u_1} {Ω₂ : Type u_2} {Ω₃ : Type u_3}    [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] [MeasurableSpace Ω₃]    {X₁ : Ω₁ → α} {X₂ : Ω₂ → α} {X₃ : Ω₃ → α}    (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hX₃ : Measurable X₃)    [FiniteRange X₁] [FiniteRange X₂] [FiniteRange X₃]    (μ₁ : Measure Ω₁) (μ₂ : Measure Ω₂) (μ₃ : Measure Ω₃)    [hμ₁ : IsProbabilityMeasure μ₁] [hμ₂ : IsProbabilityMeasure μ₂]    [hμ₃ : IsProbabilityMeasure μ₃] :    ∃ (A : Type (max u_1 u_2 u_3)) (_ : MeasurableSpace A) (μA : Measure A)      (X₁' X₂' X₃' : A → α),    IsProbabilityMeasure μA ∧    iIndepFun ![X₁', X₂', X₃'] μA ∧      Measurable X₁' ∧ Measurable X₂' ∧ Measurable X₃' ∧      IdentDistrib X₁' X₁ μA μ₁ ∧ IdentDistrib X₂' X₂ μA μ₂ ∧ IdentDistrib X₃' X₃ μA μ₃ ∧      FiniteRange X₁' ∧ FiniteRange X₂' ∧ FiniteRange X₃' := by    have : Nonempty α := μ₁.nonempty_of_neZero.map X₁    obtain ⟨A, mA, μA, X₁', X₂', X₃', hμA, hind, hX₁, hX₂, hX₃, hId₁, hId₂, hId₃⟩ :=      independent_copies3_nondep hX₁ hX₂ hX₃ μ₁ μ₂ μ₃    rcases identDistrib_of_finiteRange hX₁ hId₁.symm with ⟨X₁'', hX₁'', hX₁''_finite, hX₁''_eq⟩    rcases identDistrib_of_finiteRange hX₂ hId₂.symm with ⟨X₂'', hX₂'', hX₂''_finite, hX₂''_eq⟩    rcases identDistrib_of_finiteRange hX₃ hId₃.symm with ⟨X₃'', hX₃'', hX₃''_finite, hX₃''_eq⟩    use A, mA, μA, X₁'', X₂'', X₃''    refine ⟨hμA, ?_, hX₁'', hX₂'', hX₃'', ?_, ?_, ?_, hX₁''_finite, hX₂''_finite, hX₃''_finite⟩    · apply iIndepFun.ae_eq hind      intro i; fin_cases i      all_goals simp [hX₁''_eq.symm, hX₂''_eq.symm, hX₃''_eq.symm]    · convert IdentDistrib.trans _ hId₁      exact IdentDistrib.of_ae_eq (Measurable.aemeasurable hX₁'') hX₁''_eq    · convert IdentDistrib.trans _ hId₂      exact IdentDistrib.of_ae_eq (Measurable.aemeasurable hX₂'') hX₂''_eq    convert IdentDistrib.trans _ hId₃    exact IdentDistrib.of_ae_eq (Measurable.aemeasurable hX₃'') hX₃''_eq