Theorems · Theorem · measure theory

MeasureTheory.charFun_pi

∀ {ι : Type u_6} [inst : Fintype ι] {E : ι → Type u_7} [inst_1 : (i : ι) → NormedAddCommGroup (E i)]
  [inst_2 : (i : ι) → InnerProductSpace ℝ (E i)] {mE : (i : ι) → MeasurableSpace (E i)}
  {μ : (i : ι) → MeasureTheory.Measure (E i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] (t : PiLp 2 E),
  MeasureTheory.charFun (MeasureTheory.Measure.map (WithLp.toLp 2) (MeasureTheory.Measure.pi μ)) t =
    ∏ i, MeasureTheory.charFun (μ i) (t.ofLp i)

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

Defined in

Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

FintypeNormedAddCommGroupInnerProductSpaceMeasureTheory.SigmaFinite