Characteristic Function of a Finite Measure

This file defines the characteristic function of a finite measure on a topological vector space V.

The characteristic function of a finite measure P on V is the mapping W → ℂ, w => ∫ v, e (L v w) ∂P, where e is a continuous additive character and L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ is a bilinear map.

A typical example is V = W = ℝ and L v w = v * w.

The integral is expressed as ∫ v, char he hL w v ∂P, where char he hL w is the bounded continuous function fun v ↦ e (L v w) and he, hL are continuity hypotheses on e and L.

Main definition

TODO: give a definition of the characteristic function for standard choices of e and L.

Main statements

• ext_of_integral_char_eq: Assume e and L are non-trivial. If the integrals of char with respect to two finite measures P and P' coincide, then P = P'.

theorem MeasureTheory.ext_of_integral_char_eq {W : Type u_1} [AddCommGroup W] [Module ℝ W] [TopologicalSpace W] {e : AddChar ℝ Circle} {V : Type u_2} [AddCommGroup V] [Module ℝ V] [PseudoEMetricSpace V] [MeasurableSpace V] [BorelSpace V] [CompleteSpace V] [SecondCountableTopology V] {L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ} (he : Continuous ⇑e) (he' : e ≠ 1) (hL' : ∀ (v : V), v ≠ 0 → L v ≠ 0) (hL : Continuous fun (p : V × W) => (L p.1) p.2) {P P' : Measure V} [IsFiniteMeasure P] [IsFiniteMeasure P'] (h : ∀ (w : W), ∫ (v : V), (BoundedContinuousFunction.char he hL w) v ∂P = ∫ (v : V), (BoundedContinuousFunction.char he hL w) v ∂P') : P = P'

If the integrals of char with respect to two finite measures P and P' coincide, then P = P'.