English
There exists a positive constant C such that exp(C ||x||^2) is μ-integrable for a Gaussian μ on a complete space.
Русский
Существует положительная константа C, такая что exp(C ||x||^2) интегрируема по μ для гауссовой μ на завершенном пространстве.
LaTeX
$$$\\exists C>0,\\ Integrable(e^{C\\|x\\|^2}, μ)$$$
Lean4
/-- **Fernique's theorem**: for a Gaussian measure, there exists `C > 0` such that the function
`x ↦ exp (C * ‖x‖ ^ 2)` is integrable. -/
theorem exists_integrable_exp_sq [CompleteSpace E] (μ : Measure E) [IsGaussian μ] :
∃ C, 0 < C ∧ Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) μ := by
-- Since `μ ∗ μ.map (ContinuousLinearEquiv.neg ℝ)` is a centered Gaussian measure, it is invariant
-- under rotation. We can thus apply a version of Fernique's theorem to it.
obtain ⟨C, hC_pos, hC⟩ :
∃ C, 0 < C ∧ Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) (μ ∗ μ.map (ContinuousLinearEquiv.neg ℝ)) :=
exists_integrable_exp_sq_of_map_rotation_eq_self
(map_rotation_eq_self_of_forall_strongDual_eq_zero (integral_dual_conv_map_neg_eq_zero (μ := μ)) _)
-- We must now prove that the integrability with respect to
-- `μ ∗ μ.map (ContinuousLinearEquiv.neg ℝ)` implies integrability with respect to `μ` for
-- another constant `C' < C`.
refine ⟨C / 2, by positivity, ?_⟩
exact integrable_exp_sq_of_conv_neg μ hC (by positivity) (by simp [hC_pos])
