The Bochner measure of a Gaussian

This file identifies the measure in Bochner's theorem for the Gaussian positive-definite function

a ↦ exp (-c ‖a‖²).

With the Fourier convention exp (-2πi⟪a, q⟫), its representing measure is the image of the standard Gaussian under the dilation

q ↦ (√(2c) / (2π)) q.

The endpoint c = 0 is included: the dilation is then constant, so its image is the Dirac mass at the origin, representing the constant function 1.

Main declarations

• TauCeti.integral_fourierAtom_map_smul_stdGaussian: the Fourier transform of the dilated standard Gaussian.
• TauCeti.map_smul_stdGaussian_eq_bochnerMeasure_cexp_neg_mul_sq_norm: identification with the canonical measure chosen by Bochner's theorem.
• TauCeti.map_smul_stdGaussian_eq_bochnerMeasure_cexp_neg_sq_norm: the specialization c = 1.

References

• W. Rudin, Fourier Analysis on Groups (1962), Chapter 1.

theorem TauCeti.integral_fourierAtom_map_smul_stdGaussian {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {c : ℝ} (hc : 0 ≤ c) (a : V) : ∫ (q : V), fourierAtom a q ∂MeasureTheory.Measure.map (fun (x : V) => (√(2 * c) / (2 * Real.pi)) • x) (ProbabilityTheory.stdGaussian V) = Complex.exp (-↑(c * ‖a‖ ^ 2))

The Fourier-convention transform of the standard Gaussian dilated by √(2c) / (2π) is a ↦ exp (-c ‖a‖²).

theorem TauCeti.map_smul_stdGaussian_eq_bochnerMeasure_cexp_neg_mul_sq_norm {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {c : ℝ} (hc : 0 ≤ c) : MeasureTheory.Measure.map (fun (x : V) => (√(2 * c) / (2 * Real.pi)) • x) (ProbabilityTheory.stdGaussian V) = bochnerMeasure fun (a : V) => Complex.exp (-↑(c * ‖a‖ ^ 2))

The Bochner measure of a ↦ exp (-c ‖a‖²) is the standard Gaussian dilated by √(2c) / (2π).

theorem TauCeti.map_smul_stdGaussian_eq_bochnerMeasure_cexp_neg_sq_norm {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] : MeasureTheory.Measure.map (fun (x : V) => (√2 / (2 * Real.pi)) • x) (ProbabilityTheory.stdGaussian V) = bochnerMeasure fun (a : V) => Complex.exp (-↑(‖a‖ ^ 2))

The Bochner measure of the Gaussian acceptance example a ↦ exp (-‖a‖²) is the standard Gaussian dilated by √2 / (2π).