Theorems · Theorem · probability

ProbabilityTheory.IsGaussian.exists_integrable_exp_sq

• 1000+ list: Fernique's theorem

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [SecondCountableTopology E] [CompleteSpace E] (μ : MeasureTheory.Measure E) [ProbabilityTheory.IsGaussian μ],
  ∃ C, 0 < C ∧ MeasureTheory.Integrable (fun x => Real.exp (C * ‖x‖ ^ 2)) μ

Fernique's theorem: for a Gaussian measure, there exists C > 0 such that the function x ↦ exp (C * ‖x‖ ^ 2) is integrable.

Defined in

Mathlib.Probability.Distributions.Gaussian.Fernique

Cited by

1 results in Mathlib

Foundations

Depth 309 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceMeasurableSpaceBorelSpaceSecondCountableTopologyCompleteSpaceProbabilityTheory.IsGaussian