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

ProbabilityTheory.independent_copies'_finiteRange

PFR.ForMathlib.FiniteRange.IdentDistrib · PFR/ForMathlib/FiniteRange/IdentDistrib.lean:153 to 171

Source documentation

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

Exact Lean statement

lemma independent_copies'_finiteRange {I : Type u} [Finite I] {α : I → Type u'}
    [mS : ∀ i : I, MeasurableSpace (α i)] [mS' : ∀ i, MeasurableSingletonClass (α i)]
    [mnon: ∀ i, Nonempty (α 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)] [∀ i, FiniteRange (X 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) ∧ FiniteRange (X' i)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma independent_copies'_finiteRange {I : Type u} [Finite I] {α : I → Type u'}    [mS : ∀ i : I, MeasurableSpace (α i)] [mS' : ∀ i, MeasurableSingletonClass (α i)]    [mnon: ∀ i, Nonempty (α 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)] [∀ i, FiniteRange (X 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) ∧ FiniteRange (X' i) := by  cases nonempty_fintype I  obtain ⟨A, mA, μA, X', ⟨hμA, hindep, hident⟩⟩ := independent_copies' X hX μ  set h := fun i ↦ (identDistrib_of_finiteRange ((hident i).1) (hident i).2.symm)  choose X'' hX'' using h  refine ⟨A, mA, μA, X'', hμA, ?_, ?_⟩  · apply hindep.ae_eq    intro i    exact (hX'' i).2.2.symm  intro i  refine ⟨(hX'' i).1, ?_, (hX'' i).2.1⟩  exact .trans (.of_ae_eq (hX'' i).1.aemeasurable (hX'' i).2.2) (hident i).2