Theorems · Theorem · measure theory

MeasureTheory.Measure.ext_of_charFunDual

∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {mE : MeasurableSpace E} [BorelSpace E]
  [SecondCountableTopology E] [CompleteSpace E] {μ ν : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν], MeasureTheory.charFunDual μ = MeasureTheory.charFunDual ν → μ = ν

If two finite measures have the same characteristic function, then they are equal.

Defined in

Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Cited by

8 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceBorelSpaceSecondCountableTopologyCompleteSpaceMeasureTheory.IsFiniteMeasureMeasureTheory.IsFiniteMeasure