Theorems · Theorem · probability

ProbabilityTheory.IndepFun.charFunDual_map_add_eq_mul

∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {E : Type u_2}
  {mE : MeasurableSpace E} [inst : NormedAddCommGroup E] [BorelSpace E] [SecondCountableTopology E] {X : Ω → E}
  [inst_3 : NormedSpace ℝ E] {Y : Ω → E},
  AEMeasurable X P →
    AEMeasurable Y P →
      ProbabilityTheory.IndepFun X Y P →
        MeasureTheory.charFunDual (MeasureTheory.Measure.map (X + Y) P) =
          MeasureTheory.charFunDual (MeasureTheory.Measure.map X P) *
            MeasureTheory.charFunDual (MeasureTheory.Measure.map Y P)

Defined in

Mathlib.Probability.Independence.CharacteristicFunction

Cited by

3 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsFiniteMeasureNormedAddCommGroupBorelSpaceSecondCountableTopologyNormedSpace