Fourier inversion for measures with integrable characteristic function

A finite Borel measure whose characteristic function φ = charFun μ is integrable is absolutely continuous with respect to Lebesgue measure, with a bounded continuous density obtained by Fourier inversion of φ. On the real line the density is

f(x) = (2π)⁻¹ * Re ∫ t, exp (-i t x) * φ(t) dt,

recorded here as MeasureTheory.Measure.charFunDensity μ. This is the classical inversion theorem used to produce densities of laws that are specified through their characteristic function, such as the stable laws.

On a finite-dimensional real inner-product space V the density is stated in Mathlib's 2π Fourier convention: it is the real part of the inverse Fourier transform of v ↦ φ((-2π) • v). The proof combines the L¹ case of Bochner's theorem (TauCeti.integral_fourierAtom_withDensity_re_fourierInv), applied to this positive-definite integrable function, with uniqueness of measures with a given characteristic function.

On ℝ the density is nonnegative, continuous and bounded by (2π)⁻¹ * ∫ ‖φ‖ for every finite measure; without integrability of φ the defining integral diverges and the density is zero.

Main declarations

• MeasureTheory.Measure.eq_withDensity_re_fourierInv_charFun: a finite measure with integrable characteristic function has density (𝓕⁻ (φ ∘ ((-2π) • ·))).re.
• MeasureTheory.Measure.charFunDensity: the inversion density of a measure on ℝ.
• MeasureTheory.Measure.eq_withDensity_charFunDensity: the inversion theorem on ℝ.
• MeasureTheory.Measure.charFunDensity_nonneg, MeasureTheory.Measure.continuous_charFunDensity and MeasureTheory.Measure.charFunDensity_le: nonnegativity, continuity and the uniform bound.

References

• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. II, 2nd ed., Wiley (1971), Section XV.3, Theorem 3.

theorem MeasureTheory.Measure.eq_withDensity_re_fourierInv_charFun {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {μ : Measure V} [IsFiniteMeasure μ] (h : Integrable (charFun μ) volume) : μ = volume.withDensity fun (x : V) => ENNReal.ofReal (FourierTransformInv.fourierInv (fun (v : V) => charFun μ ((-2 * Real.pi) • v)) x).re

Fourier inversion for measures. A finite measure on a finite-dimensional real inner-product space whose characteristic function φ is integrable has density (𝓕⁻ (v ↦ φ((-2π) • v))).re with respect to Lebesgue measure.

The real line

noncomputable def MeasureTheory.Measure.charFunDensity (μ : Measure ℝ) (x : ℝ) : ℝ

The inversion density of a measure μ on ℝ with characteristic function φ: x ↦ (2π)⁻¹ * Re ∫ t, exp (-i t x) * φ(t) dt. When μ is finite and φ is integrable this is a density of μ (eq_withDensity_charFunDensity); when μ is finite and φ is not integrable, the integral diverges and the function vanishes (charFunDensity_of_not_integrable).

theorem MeasureTheory.Measure.charFunDensity_def (μ : Measure ℝ) (x : ℝ) : μ.charFunDensity x = (2 * Real.pi)⁻¹ * (∫ (t : ℝ), Complex.exp (-(↑t * ↑x * Complex.I)) * charFun μ t).re

theorem MeasureTheory.Measure.measurable_charFunDensity {α : Type u_1} [MeasurableSpace α] {μ : α → Measure ℝ} {x : α → ℝ} (hμ : Measurable fun (p : α × ℝ) => charFun (μ p.1) p.2) (hx : Measurable x) : Measurable fun (a : α) => (μ a).charFunDensity (x a)

A family's inversion density is measurable at a measurable sample point whenever its characteristic function is jointly measurable in the parameter and frequency. No finiteness or integrability assumption is needed for the totalized inversion integral.

theorem MeasureTheory.Measure.norm_cexp_mul_charFun {μ : Measure ℝ} (x t : ℝ) : ‖Complex.exp (-(↑t * ↑x * Complex.I)) * charFun μ t‖ = ‖charFun μ t‖

The Fourier phase exp (-i t x) does not change the modulus of the characteristic function.

theorem MeasureTheory.Measure.integrable_cexp_mul_charFun_iff {μ : Measure ℝ} [IsFiniteMeasure μ] (x : ℝ) : Integrable (fun (t : ℝ) => Complex.exp (-(↑t * ↑x * Complex.I)) * charFun μ t) volume ↔ Integrable (charFun μ) volume

The integrand of charFunDensity μ x is integrable exactly when the characteristic function is.

theorem MeasureTheory.Measure.charFunDensity_of_not_integrable {μ : Measure ℝ} [IsFiniteMeasure μ] (h : ¬Integrable (charFun μ) volume) (x : ℝ) : μ.charFunDensity x = 0

Without integrability of the characteristic function, the inversion density vanishes.

theorem MeasureTheory.Measure.charFunDensity_eq_re_fourierInv (μ : Measure ℝ) (x : ℝ) : μ.charFunDensity x = (FourierTransformInv.fourierInv (fun (v : ℝ) => charFun μ ((-2 * Real.pi) • v)) x).re

The inversion density is the real part of the inverse Fourier transform, in Mathlib's 2π convention, of v ↦ φ((-2π) • v): substitute t = -2πv.

theorem MeasureTheory.Measure.charFunDensity_nonneg {μ : Measure ℝ} [IsFiniteMeasure μ] (x : ℝ) : 0 ≤ μ.charFunDensity x

The inversion density of a finite measure is nonnegative everywhere.

theorem MeasureTheory.Measure.continuous_charFunDensity {μ : Measure ℝ} [IsFiniteMeasure μ] : Continuous μ.charFunDensity

The inversion density of a finite measure is continuous.

theorem MeasureTheory.Measure.charFunDensity_le (μ : Measure ℝ) (x : ℝ) : μ.charFunDensity x ≤ (2 * Real.pi)⁻¹ * ∫ (t : ℝ), ‖charFun μ t‖

The inversion density is bounded by (2π)⁻¹ times the L¹ norm of the characteristic function.

theorem MeasureTheory.Measure.eq_withDensity_charFunDensity {μ : Measure ℝ} [IsFiniteMeasure μ] (h : Integrable (charFun μ) volume) : μ = volume.withDensity fun (x : ℝ) => ENNReal.ofReal (μ.charFunDensity x)

The inversion theorem. A finite measure on ℝ with integrable characteristic function φ has the bounded continuous density x ↦ (2π)⁻¹ * Re ∫ t, exp (-i t x) * φ(t) dt with respect to Lebesgue measure.