Theorems · Theorem · probability

ProbabilityTheory.iIndepFun.charFun_map_fun_finsetSum_eq_prod

∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ι : Type u_2} {s : Finset ι} {E : Type u_3}
  [inst : MeasurableSpace E] [inst_1 : NormedAddCommGroup E] [BorelSpace E] [SecondCountableTopology E] {X : ι → Ω → E}
  [inst_4 : InnerProductSpace ℝ E],
  (∀ i ∈ s, AEMeasurable (X i) P) →
    ProbabilityTheory.iIndepFun (s.restrict X) P →
      MeasureTheory.charFun (MeasureTheory.Measure.map (fun ω => ∑ i ∈ s, X i ω) P) =
        ∏ i ∈ s, MeasureTheory.charFun (MeasureTheory.Measure.map (X i) P)

Defined in

Mathlib.Probability.Independence.CharacteristicFunction

Cited by

3 results in Mathlib

Foundations

Depth 270 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceNormedAddCommGroupBorelSpaceSecondCountableTopologyInnerProductSpace