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

ProbabilityTheory.independent_copies4_nondep_finiteRange

PFR.ForMathlib.FiniteRange.IdentDistrib · PFR/ForMathlib/FiniteRange/IdentDistrib.lean:110 to 148

Source documentation

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

Exact Lean statement

lemma independent_copies4_nondep_finiteRange {α : Type u}
    [mS : MeasurableSpace α] [MeasurableSingletonClass α]
    {Ω₁ : Type u_1} {Ω₂ : Type u_2} {Ω₃ : Type u_3} {Ω₄ : Type u_4}
    [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] [MeasurableSpace Ω₃] [MeasurableSpace Ω₄]
    {X₁ : Ω₁ → α} {X₂ : Ω₂ → α} {X₃ : Ω₃ → α} {X₄ : Ω₄ → α}
    (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hX₃ : Measurable X₃) (hX₄ : Measurable X₄)
    [FiniteRange X₁] [FiniteRange X₂] [FiniteRange X₃] [FiniteRange 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 μ₄ ∧ FiniteRange X₁' ∧ FiniteRange X₂'
      ∧ FiniteRange X₃' ∧ FiniteRange X₄'

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma independent_copies4_nondep_finiteRange {α : Type u}    [mS : MeasurableSpace α] [MeasurableSingletonClass α]    {Ω₁ : Type u_1} {Ω₂ : Type u_2} {Ω₃ : Type u_3} {Ω₄ : Type u_4}    [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] [MeasurableSpace Ω₃] [MeasurableSpace Ω₄]    {X₁ : Ω₁ → α} {X₂ : Ω₂ → α} {X₃ : Ω₃ → α} {X₄ : Ω₄ → α}    (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hX₃ : Measurable X₃) (hX₄ : Measurable X₄)    [FiniteRange X₁] [FiniteRange X₂] [FiniteRange X₃] [FiniteRange 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 μ₄ ∧ FiniteRange X₁' ∧ FiniteRange X₂'      ∧ FiniteRange X₃' ∧ FiniteRange X₄' := by    have : Nonempty α := μ₁.nonempty_of_neZero.map X₁    obtain ⟨A, mA, μA, X₁', X₂', X₃', X₄', hμA, hind, hX₁, hX₂, hX₃, hX₄, hId₁, hId₂, hId₃, hId₄⟩ :=      independent_copies4_nondep hX₁ 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⟩    rcases identDistrib_of_finiteRange hX₄ hId₄.symm with ⟨X₄'', hX₄'', hX₄''_finite, hX₄''_eq⟩    use A, mA, μA, X₁'', X₂'', X₃'', X₄''    refine ⟨hμA, ?_, hX₁'', hX₂'', hX₃'', hX₄'', ?_, ?_, ?_, ?_, hX₁''_finite, hX₂''_finite,        hX₃''_finite, hX₄''_finite⟩    · apply hind.ae_eq      intro i; fin_cases i      all_goals simp [hX₁''_eq.symm, 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    · convert IdentDistrib.trans _ hId₄      exact IdentDistrib.of_ae_eq (Measurable.aemeasurable hX₄'') hX₄''_eq