Theorems · Theorem · probability

ProbabilityTheory.iIndepFun_iff_charFunDual_pi

∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ι : Type u_2} [inst : Fintype ι]
  [MeasureTheory.IsProbabilityMeasure P] {E : ι → Type u_3} {mE : (i : ι) → MeasurableSpace (E i)}
  [inst_2 : (i : ι) → NormedAddCommGroup (E i)] [∀ (i : ι), CompleteSpace (E i)] [∀ (i : ι), BorelSpace (E i)]
  [∀ (i : ι), SecondCountableTopology (E i)] {X : (i : ι) → Ω → E i} [inst_6 : (i : ι) → NormedSpace ℝ (E i)]
  [inst_7 : DecidableEq ι],
  (∀ (i : ι), AEMeasurable (X i) P) →
    (ProbabilityTheory.iIndepFun X P ↔
      ∀ (L : StrongDual ℝ ((x : ι) → E x)),
        MeasureTheory.charFunDual (MeasureTheory.Measure.map (fun ω x => X x ω) P) L =
          ∏ i, MeasureTheory.charFunDual (MeasureTheory.Measure.map (X i) P) (L ∘SL ContinuousLinearMap.single ℝ E i))

A finite number of 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 iIndepFun_iff_charFun_pi 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

FintypeMeasureTheory.IsProbabilityMeasureNormedAddCommGroupCompleteSpaceBorelSpaceSecondCountableTopologyNormedSpaceDecidableEq