Theorems · Theorem · probability

ProbabilityTheory.indepFun_iff_charFunDual_prod

∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {E : Type u_2}
  {F : Type u_3} {mE : MeasurableSpace E} [inst : NormedAddCommGroup E] [BorelSpace E] [SecondCountableTopology E]
  {mF : MeasurableSpace F} [inst_3 : NormedAddCommGroup F] [CompleteSpace F] [BorelSpace F] [SecondCountableTopology F]
  {X : Ω → E} {Y : Ω → F} [inst_7 : NormedSpace ℝ E] [inst_8 : NormedSpace ℝ F] [CompleteSpace E],
  AEMeasurable X P →
    AEMeasurable Y P →
      (ProbabilityTheory.IndepFun X Y P ↔
        ∀ (L : StrongDual ℝ (E × F)),
          MeasureTheory.charFunDual (MeasureTheory.Measure.map (fun ω => (X ω, Y ω)) P) L =
            MeasureTheory.charFunDual (MeasureTheory.Measure.map X P) (L ∘SL ContinuousLinearMap.inl ℝ E F) *
              MeasureTheory.charFunDual (MeasureTheory.Measure.map Y P) (L ∘SL ContinuousLinearMap.inr ℝ E F))

Two random variables are independent if and only if their joint characteristic function is equal to the product of the characteristic functions. This is the version for Banach spaces, see indepFun_iff_charFun_prod for the Hilbert space version.

Defined in

Mathlib.Probability.Independence.CharacteristicFunction

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsFiniteMeasureNormedAddCommGroupBorelSpaceSecondCountableTopologyNormedAddCommGroupCompleteSpaceBorelSpaceSecondCountableTopologyNormedSpaceNormedSpaceCompleteSpace