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

ProbabilityTheory.iIndepFun.prod

PFR.Mathlib.Probability.Independence.Basic · PFR/Mathlib/Probability/Independence/Basic.lean:293 to 306

Mathematical statement

Exact Lean statement

lemma iIndepFun.prod {hf : ∀ (i : ι), Measurable (f i)} {ST : ι' → Finset ι}
    (hS : Pairwise (Disjoint on ST)) (h : iIndepFun f μ) :
    let β

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma iIndepFun.prod {hf : ∀ (i : ι), Measurable (f i)} {ST : ι' → Finset ι}    (hS : Pairwise (Disjoint on ST)) (h : iIndepFun f μ) :    let β := fun k ↦ Π i : ST k, α i    iIndepFun (β := β) (fun (k : ι') (x : Ω) (i : ST k) ↦ f i x) μ := by  let g : (i : ι') × ST i → ι := Subtype.val ∘' (Sigma.snd (α := ι'))  have hg : Injective g := by    intro x y hxy    have : ¬(Disjoint on ST) x.fst y.fst := by      refine not_forall.mpr ⟨{g y}, ?_⟩      simp      grind    exact Sigma.subtype_ext (not_ne_iff.mp ((@hS x.fst y.fst).mt this)) hxy  let m (i : ι') (j : ST i) : MeasurableSpace (α j) := n j  exact iIndepFun.pi' (m := m) (hf ∘' g) (h.precomp hg)