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 definitions

• innerProbChar: the bounded continuous map x ↦ exp(⟪x, t⟫ * I) in an inner product space. This is char for the inner product bilinear map and the additive character e = probChar.
• charFun μ t: the characteristic function of a measure μ at t in an inner product space E. This is defined as ∫ x, exp (⟪x, t⟫ * I) ∂μ, where ⟪x, t⟫ is the inner product on E. It is equal to ∫ v, innerProbChar w v ∂P (see charFun_eq_integral_innerProbChar).

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'.
• Measure.ext_of_charFun: If the characteristic functions charFun of two finite measures μ and ν on a complete second-countable inner product space coincide, then μ = ν.

noncomputable def BoundedContinuousFunction.innerProbChar {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (t : E) : BoundedContinuousFunction E ℂ

The bounded continuous map x ↦ exp(⟪x, t⟫ * I).

Equations

• BoundedContinuousFunction.innerProbChar t = BoundedContinuousFunction.char Real.continuous_probChar ⋯ t

theorem BoundedContinuousFunction.innerProbChar_apply {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (t x : E) : (innerProbChar t) x = Complex.exp (↑(inner x t) * Complex.I)

@[simp]

theorem BoundedContinuousFunction.innerProbChar_zero {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] : innerProbChar 0 = 1

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'.

noncomputable def MeasureTheory.charFun {E : Type u_2} {mE : MeasurableSpace E} [Inner ℝ E] (μ : Measure E) (t : E) : ℂ

The characteristic function of a measure in an inner product space.

Equations

• MeasureTheory.charFun μ t = ∫ (x : E), Complex.exp (↑(inner x t) * Complex.I) ∂μ

theorem MeasureTheory.charFun_apply {E : Type u_2} {mE : MeasurableSpace E} {μ : Measure E} [Inner ℝ E] (t : E) : charFun μ t = ∫ (x : E), Complex.exp (↑(inner x t) * Complex.I) ∂μ

theorem MeasureTheory.charFun_apply_real {μ : Measure ℝ} (t : ℝ) : charFun μ t = ∫ (x : ℝ), Complex.exp (↑t * ↑x * Complex.I) ∂μ

@[simp]

theorem MeasureTheory.charFun_zero {E : Type u_2} {mE : MeasurableSpace E} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (μ : Measure E) : charFun μ 0 = ↑(μ.real Set.univ)

@[simp]

theorem MeasureTheory.charFun_zero_measure {E : Type u_2} {mE : MeasurableSpace E} {t : E} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] : charFun 0 t = 0

@[simp]

theorem MeasureTheory.charFun_neg {E : Type u_2} {mE : MeasurableSpace E} {μ : Measure E} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (t : E) : charFun μ (-t) = (starRingEnd ℂ) (charFun μ t)

theorem MeasureTheory.charFun_eq_integral_innerProbChar {E : Type u_2} {mE : MeasurableSpace E} {μ : Measure E} {t : E} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] : charFun μ t = ∫ (v : E), (BoundedContinuousFunction.innerProbChar t) v ∂μ

charFun as the integral of a bounded continuous function.

theorem MeasureTheory.charFun_eq_integral_probChar {E : Type u_2} {mE : MeasurableSpace E} {μ : Measure E} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (t : E) : charFun μ t = ∫ (x : E), ↑(Real.probChar (inner x t)) ∂μ

theorem MeasureTheory.charFun_eq_fourierIntegral {E : Type u_2} {mE : MeasurableSpace E} {μ : Measure E} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (t : E) : charFun μ t = VectorFourier.fourierIntegral Real.probChar μ bilinFormOfRealInner 1 (-t)

charFun is a Fourier integral for the inner product and the character probChar.

theorem MeasureTheory.charFun_eq_fourierIntegral' {E : Type u_2} {mE : MeasurableSpace E} {μ : Measure E} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (t : E) : charFun μ t = VectorFourier.fourierIntegral Real.fourierChar μ bilinFormOfRealInner 1 (-(2 * Real.pi)⁻¹ • t)

charFun is a Fourier integral for the inner product and the character fourierChar.

theorem MeasureTheory.norm_charFun_le {E : Type u_2} {mE : MeasurableSpace E} {μ : Measure E} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (t : E) : ‖charFun μ t‖ ≤ μ.real Set.univ

theorem MeasureTheory.norm_charFun_le_one {E : Type u_2} {mE : MeasurableSpace E} {μ : Measure E} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [IsProbabilityMeasure μ] (t : E) : ‖charFun μ t‖ ≤ 1

theorem MeasureTheory.norm_one_sub_charFun_le_two {E : Type u_2} {mE : MeasurableSpace E} {μ : Measure E} {t : E} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [IsProbabilityMeasure μ] : ‖1 - charFun μ t‖ ≤ 2

theorem MeasureTheory.stronglyMeasurable_charFun {E : Type u_2} {mE : MeasurableSpace E} {μ : Measure E} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [OpensMeasurableSpace E] [SecondCountableTopology E] [SFinite μ] : StronglyMeasurable (charFun μ)

theorem MeasureTheory.measurable_charFun {E : Type u_2} {mE : MeasurableSpace E} {μ : Measure E} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [OpensMeasurableSpace E] [SecondCountableTopology E] [SFinite μ] : Measurable (charFun μ)

theorem MeasureTheory.intervalIntegrable_charFun {μ : Measure ℝ} [IsFiniteMeasure μ] {a b : ℝ} : IntervalIntegrable (charFun μ) volume a b

theorem MeasureTheory.charFun_map_smul {E : Type u_2} {mE : MeasurableSpace E} {μ : Measure E} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] (r : ℝ) (t : E) : charFun (Measure.map (fun (x : E) => r • x) μ) t = charFun μ (r • t)

theorem MeasureTheory.charFun_map_mul {μ : Measure ℝ} (r t : ℝ) : charFun (Measure.map (fun (x : ℝ) => r * x) μ) t = charFun μ (r * t)

theorem MeasureTheory.Measure.ext_of_charFun {E : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [BorelSpace E] [SecondCountableTopology E] {μ ν : Measure E} [IsFiniteMeasure μ] [IsFiniteMeasure ν] (h : charFun μ = charFun ν) : μ = ν

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