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 mapx ↦ exp(⟪x, t⟫ * I)in an inner product space. This ischarfor the inner product bilinear map and the additive charactere = probChar.charFun μ t: the characteristic function of a measureμattin an inner product spaceE. This is defined as∫ x, exp (⟪x, t⟫ * I) ∂μ, where⟪x, t⟫is the inner product onE. It is equal to∫ v, innerProbChar w v ∂P(seecharFun_eq_integral_innerProbChar).probCharDual: the bounded continuous mapx ↦ exp (L x * I), for a continuous linear formL.charFunDual μ L: the characteristic function of a measureμatL : Dual ℝ Ein a normed spaceE. This is the integral∫ v, exp (L v * I) ∂μ.
Main statements #
ext_of_integral_char_eq: AssumeeandLare non-trivial. If the integrals ofcharwith respect to two finite measuresPandP'coincide, thenP = P'.Measure.ext_of_charFun: If the characteristic functionscharFunof two finite measuresμandνon a complete second-countable inner product space coincide, thenμ = ν.Measure.ext_of_charFunDual: If the characteristic functionscharFunDualof two finite measuresμandνon a Banach space coincide, thenμ = ν.
The bounded continuous map x ↦ exp(⟪x, t⟫ * I).
Equations
Instances For
The bounded continuous map x ↦ exp (L x * I), for a continuous linear form L.
Equations
Instances For
If the integrals of char with respect to two finite measures P and P' coincide, then
P = P'.
The characteristic function of a measure in an inner product space.
Equations
- MeasureTheory.charFun μ t = ∫ (x : E), Complex.exp (↑(inner ℝ x t) * Complex.I) ∂μ
Instances For
charFun as the integral of a bounded continuous function.
charFun is a Fourier integral for the inner product and the character probChar.
charFun is a Fourier integral for the inner product and the character fourierChar.
If the characteristic functions charFun of two finite measures μ and ν on
a complete second-countable inner product space coincide, then μ = ν.
The characteristic function of a convolution of measures is the product of the respective characteristic functions.
The characteristic function of a product of measures is a product of
characteristic functions. This is the version for Hilbert spaces, see charFunDual_prod
for the Banach space version.
The characteristic function of a measure is a product of
characteristic functions if and only if it is a product measure.
This is the version for Hilbert spaces, see charFunDual_eq_prod_iff
for the Banach space version.
The characteristic function of a product of measures is a product of
characteristic functions. This is the version for Hilbert spaces, see charFunDual_pi
for the Banach space version.
The characteristic function of a measure is a product of
characteristic functions if and only if it is a product measure.
This is the version for Hilbert spaces, see charFunDual_eq_pi_iff
for the Banach space version.
The characteristic function of a measure in a normed space, function from StrongDual ℝ E to
ℂ with charFunDual μ L = ∫ v, exp (L v * I) ∂μ.
Equations
- MeasureTheory.charFunDual μ L = ∫ (v : E), (BoundedContinuousFunction.probCharDual L) v ∂μ
Instances For
The characteristic function of a product of measures is a product of
characteristic functions. This is the version for Banach spaces, see charFun_prod
for the Hilbert space version.
The characteristic function of a product of measures is a product of
characteristic functions. This is charFunDual_prod for WithLp.
See charFun_prod for the Hilbert space version.
The characteristic function of a product of measures is a product of
characteristic functions. This is the version for Banach spaces, see charFunDual_pi
for the Hilbert space version.
The characteristic function of a product of measures is a product of
characteristic functions. This is charFunDual_pi for PiLp.
See charFunDual_pi for the Banach space version.
If two finite measures have the same characteristic function, then they are equal.
The characteristic function of a measure is a product of
characteristic functions if and only if it is a product measure.
This is the version for Banach spaces, see charFun_eq_prod_iff
for the Hilbert space version.
The characteristic function of a measure is a product of
characteristic functions if and only if it is a product measure.
This is charFunDual_eq_prod_iff for WithLp.
See charFun_eq_prod_iff for the Hilbert space version.
The characteristic function of a measure is a product of
characteristic functions if and only if it is a product measure.
This is the version for Banach spaces, see charFun_eq_pi_iff
for the Hilbert space version.
The characteristic function of a measure is a product of
characteristic functions if and only if it is a product measure.
This is charFunDual_eq_pi_iff for PiLp.
See charFun_eq_pi_iff for the Hilbert space version.
The characteristic function of a convolution of measures is the product of the respective characteristic functions.