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

ProbabilityTheory.independent_copies4_nondep

PFR.Mathlib.Probability.IdentDistrib · PFR/Mathlib/Probability/IdentDistrib.lean:329 to 374

Source documentation

A version with exactly 4 random variables that have the same codomain. It's unfortunately incredibly painful to prove this from the general case.

Exact Lean statement

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

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma independent_copies4_nondep {α : Type u}    [mS : MeasurableSpace α]    {Ω₁ : Type u_1} {Ω₂ : Type u_2} {Ω₃ : Type u_3} {Ω₄ : Type u_4}    [mΩ₁ : MeasurableSpace Ω₁] [mΩ₂ : MeasurableSpace Ω₂]    [mΩ₃ : MeasurableSpace Ω₃] [mΩ₄ : MeasurableSpace Ω₄]    {X₁ : Ω₁ → α} {X₂ : Ω₂ → α} {X₃ : Ω₃ → α} {X₄ : Ω₄ → α}    (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hX₃ : Measurable X₃) (hX₄ : Measurable X₄)    (μ₁ : Measure Ω₁) (μ₂ : Measure Ω₂) (μ₃ : Measure Ω₃) (μ₄ : Measure Ω₄)    [hμ₁ : IsProbabilityMeasure μ₁] [hμ₂ : IsProbabilityMeasure μ₂]    [hμ₃ : IsProbabilityMeasure μ₃] [hμ₄ : IsProbabilityMeasure μ₄] :    ∃ (A : Type (max u_1 u_2 u_3 u_4)) (_ : MeasurableSpace A) (μA : Measure A)      (X₁' X₂' X₃' X₄' : A → α),    IsProbabilityMeasure μA ∧ iIndepFun ![X₁', X₂', X₃', X₄'] μA ∧    Measurable X₁' ∧ Measurable X₂' ∧ Measurable X₃' ∧ Measurable X₄' ∧    IdentDistrib X₁' X₁ μA μ₁ ∧ IdentDistrib X₂' X₂ μA μ₂ ∧    IdentDistrib X₃' X₃ μA μ₃ ∧ IdentDistrib X₄' X₄ μA μ₄ := by  let Ω₁' : Type (max u_1 u_2 u_3 u_4) := ULift.{max u_2 u_3 u_4} Ω₁  let Ω₂' : Type (max u_1 u_2 u_3 u_4) := ULift.{max u_1 u_3 u_4} Ω₂  let Ω₃' : Type (max u_1 u_2 u_3 u_4) := ULift.{max u_1 u_2 u_4} Ω₃  let Ω₄' : Type (max u_1 u_2 u_3 u_4) := ULift.{max u_1 u_2 u_3} Ω₄  let Ω : Fin 4 → Type (max u_1 u_2 u_3 u_4) := ![Ω₁', Ω₂', Ω₃', Ω₄']  let mΩ : (i : Fin 4) → MeasurableSpace (Ω i) :=    Fin.cases (inferInstance : MeasurableSpace Ω₁') <|    Fin.cases (inferInstance : MeasurableSpace Ω₂') <|    Fin.cases (inferInstance : MeasurableSpace Ω₃') <|    Fin.cases (inferInstance : MeasurableSpace Ω₄') Fin.rec0  let X : (i : Fin 4) → Ω i → α :=    Fin.cases (X₁ ∘ ULift.down) <| Fin.cases (X₂ ∘ ULift.down) <|    Fin.cases (X₃ ∘ ULift.down) <| Fin.cases (X₄ ∘ ULift.down) Fin.rec0  have hX : ∀ (i : Fin 4), @Measurable _ _ (mΩ i) mS (X i) :=    Fin.cases (hX₁.comp measurable_down) <| Fin.cases (hX₂.comp measurable_down) <|    Fin.cases (hX₃.comp measurable_down) <| Fin.cases (hX₄.comp measurable_down) Fin.rec0  let μ : (i : Fin 4) → @Measure (Ω i) (mΩ i) :=    Fin.cases (μ₁.comap ULift.down) <| Fin.cases (μ₂.comap ULift.down) <|    Fin.cases (μ₃.comap ULift.down) <| Fin.cases (μ₄.comap ULift.down) Fin.rec0  let hμ : (i : Fin 4) → IsProbabilityMeasure (μ i) :=    Fin.cases isProbabilityMeasure_comap_down <| Fin.cases isProbabilityMeasure_comap_down <|    Fin.cases isProbabilityMeasure_comap_down <| Fin.cases isProbabilityMeasure_comap_down Fin.rec0  obtain ⟨A, mA, μA, X', hμ, hi, hX'⟩ := independent_copies' X hX μ  refine ⟨A, mA, μA, X' 0, X' 1, X' 2, X' 3, hμ, ?_,    (hX' 0).1, (hX' 1).1, (hX' 2).1, (hX' 3).1,    (hX' 0).2.trans ((identDistrib_ulift_self hX₁).symm),    (hX' 1).2.trans ((identDistrib_ulift_self hX₂).symm),    (hX' 2).2.trans ((identDistrib_ulift_self hX₃).symm),    (hX' 3).2.trans ((identDistrib_ulift_self hX₄).symm)⟩  convert hi; ext i; fin_cases i <;> rfl