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

ProbabilityTheory.independent_copies3_nondep

PFR.Mathlib.Probability.IdentDistrib · PFR/Mathlib/Probability/IdentDistrib.lean:285 to 325

Source documentation

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

Exact Lean statement

lemma independent_copies3_nondep {α : Type u}
    [mS : MeasurableSpace α]
    {Ω₁ : Type u_1} {Ω₂ : Type u_2} {Ω₃ : Type u_3}
    [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] [MeasurableSpace Ω₃]
    {X₁ : Ω₁ → α} {X₂ : Ω₂ → α} {X₃ : Ω₃ → α}
    (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hX₃ : Measurable X₃)
    (μ₁ : Measure Ω₁) (μ₂ : Measure Ω₂) (μ₃ : Measure Ω₃)
    [IsProbabilityMeasure μ₁] [IsProbabilityMeasure μ₂] [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 μ₃

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma independent_copies3_nondep {α : Type u}    [mS : MeasurableSpace α]    {Ω₁ : Type u_1} {Ω₂ : Type u_2} {Ω₃ : Type u_3}    [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] [MeasurableSpace Ω₃]    {X₁ : Ω₁ → α} {X₂ : Ω₂ → α} {X₃ : Ω₃ → α}    (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hX₃ : Measurable X₃)    (μ₁ : Measure Ω₁) (μ₂ : Measure Ω₂) (μ₃ : Measure Ω₃)    [IsProbabilityMeasure μ₁] [IsProbabilityMeasure μ₂] [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 μ₃ := by  let Ω₁' : Type (max u_1 u_2 u_3) := ULift.{max u_2 u_3} Ω₁  let Ω₂' : Type (max u_1 u_2 u_3) := ULift.{max u_1 u_3} Ω₂  let Ω₃' : Type (max u_1 u_2 u_3) := ULift.{max u_1 u_2} Ω₃  let Ω : Fin 3 → Type (max u_1 u_2 u_3) := ![Ω₁', Ω₂', Ω₃']  let mΩ : (i : Fin 3) → MeasurableSpace (Ω i) :=    Fin.cases (inferInstance : MeasurableSpace Ω₁') <|    Fin.cases (inferInstance : MeasurableSpace Ω₂') <|    Fin.cases (inferInstance : MeasurableSpace Ω₃') Fin.rec0  let X : (i : Fin 3) → Ω i → α := Fin.cases (X₁ ∘ ULift.down) <| Fin.cases (X₂ ∘ ULift.down) <|    Fin.cases (X₃ ∘ ULift.down) Fin.rec0  have hX : ∀ (i : Fin 3), @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.rec0  let μ : (i : Fin 3) → @Measure (Ω i) (mΩ i) :=    Fin.cases (μ₁.comap ULift.down) <|    Fin.cases (μ₂.comap ULift.down) <|    Fin.cases (μ₃.comap ULift.down) Fin.rec0  have hμ : (i : Fin 3) → IsProbabilityMeasure (μ i) :=    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, hμ, ?_,    (hX' 0).1, (hX' 1).1, (hX' 2).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⟩  convert hi; ext i; fin_cases i <;> rfl