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

ProbabilityTheory.IdentDistrib.iprodMk

PFR.Mathlib.Probability.IdentDistrib · PFR/Mathlib/Probability/IdentDistrib.lean:142 to 160

Mathematical statement

Exact Lean statement

theorem IdentDistrib.iprodMk {I : Type*} [Finite I] {F : I → Ω → β} {F' : I → Ω' → β}
    (hFF' : ∀ i, IdentDistrib (F i) (F' i) μ ν) (hμ : IsProbabilityMeasure μ)
    (hν : IsProbabilityMeasure ν) (h : iIndepFun F μ) (h' : iIndepFun F' ν) :
    IdentDistrib (fun x i ↦ F i x) (fun x i ↦ F' i x) μ ν where
  aemeasurable_fst

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem IdentDistrib.iprodMk {I : Type*} [Finite I] {F : I → Ω → β} {F' : I → Ω' → β}    (hFF' : ∀ i, IdentDistrib (F i) (F' i) μ ν) (hμ : IsProbabilityMeasure μ)    (hν : IsProbabilityMeasure ν) (h : iIndepFun F μ) (h' : iIndepFun F' ν) :    IdentDistrib (fun x i ↦ F i x) (fun x i ↦ F' i x) μ ν where  aemeasurable_fst := by    apply AEMeasurable.piMk    intro i; exact (hFF' i).aemeasurable_fst  aemeasurable_snd := by    apply AEMeasurable.piMk    intro i; exact (hFF' i).aemeasurable_snd  map_eq := by    cases nonempty_fintype I    rw [iIndepFun_iff_map_fun_eq_pi_map] at h h'    · rw [h,h']      congr      ext i : 1      exact (hFF' i).map_eq    · intro i; exact (hFF' i).aemeasurable_snd    intro i; exact (hFF' i).aemeasurable_fst