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

ProbabilityTheory.independent_copies'

PFR.Mathlib.Probability.IdentDistrib · PFR/Mathlib/Probability/IdentDistrib.lean:265 to 281

Source documentation

Let Xᵢ : Ωᵢ → Sᵢ be random variables for i = 1,...,k. Then there exist jointly independent random variables Xᵢ' : Ω' → Sᵢ for i=1,...,k such that each Xᵢ' is a copy of Xᵢ.

Exact Lean statement

lemma independent_copies' {I : Type u} [Finite I] {α : I → Type u'}
    [mS : ∀ i : I, MeasurableSpace (α i)] {Ω : I → Type v}
    [mΩ : ∀ i : I, MeasurableSpace (Ω i)] (X : ∀ i : I, Ω i → α i) (hX : ∀ i : I, Measurable (X i))
    (μ : ∀ i : I, Measure (Ω i)) [∀ i, IsProbabilityMeasure (μ i)] :
    ∃ (A : Type (max u v)) (_ : MeasurableSpace A) (μA : Measure A) (X' : ∀ i, A → α i),
    IsProbabilityMeasure μA ∧ iIndepFun X' μA ∧
    ∀ i : I, Measurable (X' i) ∧ IdentDistrib (X' i) (X i) μA (μ i)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma independent_copies' {I : Type u} [Finite I] {α : I → Type u'}    [mS : ∀ i : I, MeasurableSpace (α i)] {Ω : I → Type v}    [mΩ : ∀ i : I, MeasurableSpace (Ω i)] (X : ∀ i : I, Ω i → α i) (hX : ∀ i : I, Measurable (X i))    (μ : ∀ i : I, Measure (Ω i)) [∀ i, IsProbabilityMeasure (μ i)] :    ∃ (A : Type (max u v)) (_ : MeasurableSpace A) (μA : Measure A) (X' : ∀ i, A → α i),    IsProbabilityMeasure μA ∧ iIndepFun X' μA ∧    ∀ i : I, Measurable (X' i) ∧ IdentDistrib (X' i) (X i) μA (μ i) := by  cases nonempty_fintype I  refine ⟨Π i, Ω i, inferInstance, .pi μ, fun i ↦ X i ∘ eval i, inferInstance, ?_, fun i ↦ ⟨?_, ?_⟩⟩  · rw [iIndepFun_iff]    intro t s hs    choose! u _ hus using hs    simp +contextual only [← hus, preimage_comp, pi_eval_preimage]    simp_rw [← Finset.mem_coe, ← Set.pi_def, pi_pi_finset]  · exact (hX i).comp (measurable_pi_apply i)  · refine ⟨(hX i).comp (measurable_pi_apply i) |>.aemeasurable, (hX i).aemeasurable, ?_⟩    rw [← Measure.map_map (hX i) (measurable_pi_apply i), Measure.map_eval_pi]