Theorems · Theorem · measure theory

MeasureTheory.charFunDual_pi

∀ {ι : Type u_4} [inst : Fintype ι] [inst_1 : DecidableEq ι] {E : ι → Type u_5}
  [inst_2 : (i : ι) → NormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace ℝ (E i)]
  {mE : (i : ι) → MeasurableSpace (E i)} {μ : (i : ι) → MeasureTheory.Measure (E i)}
  [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] (L : StrongDual ℝ ((i : ι) → E i)),
  MeasureTheory.charFunDual (MeasureTheory.Measure.pi μ) L =
    ∏ i, MeasureTheory.charFunDual (μ i) (L ∘SL ContinuousLinearMap.single ℝ E i)

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

Defined in

Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

FintypeDecidableEqNormedAddCommGroupNormedSpaceMeasureTheory.SigmaFinite