Theorems · Theorem · probability

ProbabilityTheory.Fernique.logRatio_mul_normThreshold_add_one_le

∀ {a : ℝ} {c : ENNReal},
  2⁻¹ < c →
    c < 1 →
      ∀ (n : ℕ),
        ProbabilityTheory.Fernique.logRatio c * ProbabilityTheory.Fernique.normThreshold a (n + 1) ^ 2 * a⁻¹ ^ 2 ≤
          2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * 2 ^ n

Defined in: Mathlib.Probability.Distributions.Fernique
Cited by: 1 results in Mathlib
Foundations: Depth 176 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites43

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement and proof · cited by 25,697
ENNRealstatement and proof · cited by 9,879
Top.topproof · cited by 9,680
mul_oneproof · cited by 3,885
one_mulproof · cited by 2,841
Nat.cast_oneproof · cited by 2,501
mul_commproof · cited by 2,262
LT.lt.leproof · cited by 2,189
MulZeroClass.mul_zeroproof · cited by 2,091
Nat.cast_zeroproof · cited by 1,870
le_of_ltproof · cited by 1,175
Real.logstatement and proof · cited by 939

Cited by1

Results whose statement or proof uses this declaration.

ProbabilityTheory.Fernique.lintegral_closedBall_sdiff_exp_logRatio_mul_sq_leproof · cited by 2