Theorems · Theorem · measure theory

MeasureTheory.Measure.ext_of_charFun

∀ {E : Type u_3} [inst : MeasurableSpace E] {μ ν : MeasureTheory.Measure E} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E]
  [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν],
  MeasureTheory.charFun μ = MeasureTheory.charFun ν → μ = ν

If the characteristic functions charFun of two finite measures μ and ν on a complete second-countable inner product space coincide, then μ = ν.

Defined in

Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Cited by

7 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceNormedAddCommGroupInnerProductSpaceBorelSpaceSecondCountableTopologyCompleteSpaceMeasureTheory.IsFiniteMeasureMeasureTheory.IsFiniteMeasure