Theorems · Theorem · probability

ProbabilityTheory.Fernique.lintegral_closedBall_sdiff_exp_logRatio_mul_sq_le

∀ {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 μ →
    2⁻¹ < μ {x | ‖x‖ ≤ a} →
      μ {x | ‖x‖ ≤ a} < 1 →
        ∀ (n : ℕ),
          ∫⁻ (x : E) in
              Metric.closedBall 0 (ProbabilityTheory.Fernique.normThreshold a (n + 1)) \
                Metric.closedBall 0 (ProbabilityTheory.Fernique.normThreshold a n),
              ENNReal.ofReal (Real.exp (ProbabilityTheory.Fernique.logRatio (μ {x | ‖x‖ ≤ a}) * a⁻¹ ^ 2 * ‖x‖ ^ 2)) ∂μ ≤
            μ {x | ‖x‖ ≤ a} *
              ENNReal.ofReal (Real.exp (-2⁻¹ * Real.log (μ {x | ‖x‖ ≤ a} / (1 - μ {x | ‖x‖ ≤ a})).toReal * 2 ^ n))

Auxiliary lemma for lintegral_exp_mul_sq_norm_le_mul, in which we find an upper bound on an integral by dealing separately with the contribution of each set in a sequence of annuli. This is the bound of the integral over one of those annuli.

Defined in

Mathlib.Probability.Distributions.Fernique

Cited by

2 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupNormedSpaceSecondCountableTopologyMeasurableSpaceBorelSpaceMeasureTheory.IsProbabilityMeasure