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).
• probCharDual: the bounded continuous map x ↦ exp (L x * I), for a continuous linear form L.
• charFunDual μ L: the characteristic function of a measure μ at L : Dual ℝ E in a normed space E. This is the integral ∫ v, exp (L v * I) ∂μ.

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 μ = ν.
• Measure.ext_of_charFunDual: If the characteristic functions charFunDual of two finite measures μ and ν on a Banach 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

noncomputable def BoundedContinuousFunction.probCharDual {F : Type u_2} [SeminormedAddCommGroup F] [NormedSpace ℝ F] (L : NormedSpace.Dual ℝ F) : BoundedContinuousFunction F ℂ

The bounded continuous map x ↦ exp (L x * I), for a continuous linear form L.

Equations

• BoundedContinuousFunction.probCharDual L = BoundedContinuousFunction.char Real.continuous_probChar ⋯ L

theorem BoundedContinuousFunction.probCharDual_apply {F : Type u_2} [SeminormedAddCommGroup F] [NormedSpace ℝ F] (L : NormedSpace.Dual ℝ F) (x : F) : (probCharDual L) x = Complex.exp (↑(L x) * Complex.I)

@[simp]

theorem BoundedContinuousFunction.probCharDual_zero {F : Type u_2} [SeminormedAddCommGroup F] [NormedSpace ℝ F] : probCharDual 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)

@[simp]

theorem MeasureTheory.charFun_dirac {E : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [OpensMeasurableSpace E] {x : E} (t : E) : charFun (Measure.dirac x) t = Complex.exp (↑(inner ℝ x t) * Complex.I)

theorem MeasureTheory.charFun_map_add_const {E : Type u_3} [MeasurableSpace E] {μ : Measure E} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [BorelSpace E] (r t : E) : charFun (Measure.map (fun (x : E) => x + r) μ) t = charFun μ t * Complex.exp (↑(inner ℝ r t) * Complex.I)

theorem MeasureTheory.charFun_map_const_add {E : Type u_3} [MeasurableSpace E] {μ : Measure E} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [BorelSpace E] (r t : E) : charFun (Measure.map (fun (x : E) => r + x) μ) t = charFun μ t * Complex.exp (↑(inner ℝ r t) * Complex.I)

theorem MeasureTheory.Measure.ext_of_charFun {E : Type u_3} [MeasurableSpace E] {μ ν : Measure E} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace 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 μ = ν.

theorem MeasureTheory.charFun_conv {E : Type u_3} [MeasurableSpace E] {μ ν : Measure E} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] [IsFiniteMeasure μ] [IsFiniteMeasure ν] (t : E) : charFun (μ.conv ν) t = charFun μ t * charFun ν t

The characteristic function of a convolution of measures is the product of the respective characteristic functions.

noncomputable def MeasureTheory.charFunDual {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {mE : MeasurableSpace E} (μ : Measure E) (L : NormedSpace.Dual ℝ E) : ℂ

The characteristic function of a measure in a normed space, function from Dual ℝ E to ℂ with charFunDual μ L = ∫ v, exp (L v * I) ∂μ.

Equations

• MeasureTheory.charFunDual μ L = ∫ (v : E), (BoundedContinuousFunction.probCharDual L) v ∂μ

theorem MeasureTheory.charFunDual_apply {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {mE : MeasurableSpace E} {μ : Measure E} (L : NormedSpace.Dual ℝ E) : charFunDual μ L = ∫ (v : E), Complex.exp (↑(L v) * Complex.I) ∂μ

theorem MeasureTheory.charFunDual_eq_charFun_map_one {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {mE : MeasurableSpace E} {μ : Measure E} [OpensMeasurableSpace E] (L : NormedSpace.Dual ℝ E) : charFunDual μ L = charFun (Measure.map (⇑L) μ) 1

theorem MeasureTheory.charFun_map_eq_charFunDual_smul {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {mE : MeasurableSpace E} {μ : Measure E} [OpensMeasurableSpace E] (L : NormedSpace.Dual ℝ E) (u : ℝ) : charFun (Measure.map (⇑L) μ) u = charFunDual μ (u • L)

theorem MeasureTheory.charFun_eq_charFunDual_toDualMap {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {mE : MeasurableSpace E} {μ : Measure E} (t : E) : charFun μ t = charFunDual μ ((InnerProductSpace.toDualMap ℝ E) t)

theorem MeasureTheory.charFunDual_map {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {mE : MeasurableSpace E} [NormedAddCommGroup F] [NormedSpace ℝ F] {mF : MeasurableSpace F} {μ : Measure E} [OpensMeasurableSpace E] [BorelSpace F] (L : E →L[ℝ] F) (L' : NormedSpace.Dual ℝ F) : charFunDual (Measure.map (⇑L) μ) L' = charFunDual μ (ContinuousLinearMap.comp L' L)

@[simp]

theorem MeasureTheory.charFunDual_dirac {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {mE : MeasurableSpace E} [OpensMeasurableSpace E] {x : E} (L : NormedSpace.Dual ℝ E) : charFunDual (Measure.dirac x) L = Complex.exp (↑(L x) * Complex.I)

theorem MeasureTheory.charFunDual_map_add_const {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {mE : MeasurableSpace E} {μ : Measure E} [BorelSpace E] (r : E) (L : NormedSpace.Dual ℝ E) : charFunDual (Measure.map (fun (x : E) => x + r) μ) L = charFunDual μ L * Complex.exp (↑(L r) * Complex.I)

theorem MeasureTheory.charFunDual_map_const_add {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {mE : MeasurableSpace E} {μ : Measure E} [BorelSpace E] (r : E) (L : NormedSpace.Dual ℝ E) : charFunDual (Measure.map (fun (x : E) => r + x) μ) L = charFunDual μ L * Complex.exp (↑(L r) * Complex.I)

theorem MeasureTheory.charFunDual_prod {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {mE : MeasurableSpace E} [NormedAddCommGroup F] [NormedSpace ℝ F] {mF : MeasurableSpace F} {μ : Measure E} {ν : Measure F} [SFinite μ] [SFinite ν] (L : NormedSpace.Dual ℝ (E × F)) : charFunDual (μ.prod ν) L = charFunDual μ (ContinuousLinearMap.comp L (ContinuousLinearMap.inl ℝ E F)) * charFunDual ν (ContinuousLinearMap.comp L (ContinuousLinearMap.inr ℝ E F))

The characteristic function of a product of measures is a product of characteristic functions.

theorem MeasureTheory.Measure.ext_of_charFunDual {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {mE : MeasurableSpace E} [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] {μ ν : Measure E} [IsFiniteMeasure μ] [IsFiniteMeasure ν] (h : charFunDual μ = charFunDual ν) : μ = ν

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

theorem MeasureTheory.charFunDual_conv {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {mE : MeasurableSpace E} [BorelSpace E] [SecondCountableTopology E] {μ ν : Measure E} [IsFiniteMeasure μ] [IsFiniteMeasure ν] (L : NormedSpace.Dual ℝ E) : charFunDual (μ.conv ν) L = charFunDual μ L * charFunDual ν L

The characteristic function of a convolution of measures is the product of the respective characteristic functions.