Theorems · Theorem · measure theory

MeasureTheory.charFunDual_prod

∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {mE : MeasurableSpace E}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {mF : MeasurableSpace F} {μ : MeasureTheory.Measure E}
  {ν : MeasureTheory.Measure F} [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] (L : StrongDual ℝ (E × F)),
  MeasureTheory.charFunDual (μ.prod ν) L =
    MeasureTheory.charFunDual μ (L ∘SL ContinuousLinearMap.inl ℝ E F) *
      MeasureTheory.charFunDual ν (L ∘SL ContinuousLinearMap.inr ℝ E F)

The characteristic function of a product of measures is a product of characteristic functions. This is the version for Banach spaces, see charFun_prod for the Hilbert space version.

Defined in

Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceMeasureTheory.SFiniteMeasureTheory.SFinite