Theorems · Theorem · measure theory

MeasureTheory.charFun_prod

∀ {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : InnerProductSpace ℝ F] {mE : MeasurableSpace E} {mF : MeasurableSpace F}
  {μ : MeasureTheory.Measure E} {ν : MeasureTheory.Measure F} [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν]
  (t : WithLp 2 (E × F)),
  MeasureTheory.charFun (MeasureTheory.Measure.map (WithLp.toLp 2) (μ.prod ν)) t =
    MeasureTheory.charFun μ t.ofLp.1 * MeasureTheory.charFun ν t.ofLp.2

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

Defined in

Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedAddCommGroupInnerProductSpaceInnerProductSpaceMeasureTheory.SFiniteMeasureTheory.SFinite