Theorems · Theorem · probability

ProbabilityTheory.IsGaussian.integrable_exp_sq_of_conv_neg

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

If x ↦ exp (C * ‖x‖ ^ 2) is integrable with respect to the centered Gaussian μ ∗ (μ.map (ContinuousLinearEquiv.neg ℝ)), then for all C' < C, x ↦ exp (C' * ‖x‖ ^ 2) is integrable with respect to μ.

Defined in

Mathlib.Probability.Distributions.Gaussian.Fernique

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceMeasurableSpaceBorelSpaceSecondCountableTopologyProbabilityTheory.IsGaussian