Theorems · Theorem · probability

ProbabilityTheory.lintegral_exp_mul_sq_norm_le_of_map_rotation_eq_self

∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [SecondCountableTopology E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} {a : ℝ}
  [MeasureTheory.IsProbabilityMeasure μ],
  MeasureTheory.Measure.map (⇑(ContinuousLinearMap.rotation (-(Real.pi / 4)))) (μ.prod μ) = μ.prod μ →
    ∀ {c : ENNReal},
      c ≤ μ {x | ‖x‖ ≤ a} →
        2⁻¹ < c →
          ∫⁻ (x : E), ENNReal.ofReal (Real.exp (ProbabilityTheory.Fernique.logRatio c * a⁻¹ ^ 2 * ‖x‖ ^ 2)) ∂μ ≤
            ENNReal.ofReal (Real.exp (ProbabilityTheory.Fernique.logRatio c)) +
              ∑' (n : ℕ), ENNReal.ofReal (Real.exp (-2⁻¹ * Real.log (c / (1 - c)).toReal * 2 ^ n))

For μ a probability measure whose product with itself is invariant by rotation and for a, c with 2⁻¹ < c ≤ μ {x | ‖x‖ ≤ a}, the integral ∫⁻ x, exp (logRatio c * a⁻¹ ^ 2 * ‖x‖ ^ 2) ∂μ is bounded by a quantity that does not depend on a.

Defined in

Mathlib.Probability.Distributions.Fernique

Cited by

1 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupNormedSpaceSecondCountableTopologyMeasurableSpaceBorelSpaceMeasureTheory.IsProbabilityMeasure