Theorems · Theorem · probability
ProbabilityTheory.Fernique.logRatio_nonneg
∀ {c : ENNReal}, 2⁻¹ ≤ c → c ≤ 1 → 0 ≤ ProbabilityTheory.Fernique.logRatio c- Cited by
- 2 results in Mathlib
- Foundations
- Depth 176 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites18
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- ENNRealstatement and proof · cited by 9,879
- LT.lt.leproof · cited by 2,189
- Real.logproof · cited by 939
- ENNReal.toRealproof · cited by 859
- Real.sqrtproof · cited by 545
- div_zeroproof · cited by 251
- div_selfproof · cited by 237
- zero_divproof · cited by 222
- tsub_selfproof · cited by 154
- Real.log_oneproof · cited by 91
- Real.log_zeroproof · cited by 84
Cited by2
Results whose statement or proof uses this declaration.
- ProbabilityTheory.lintegral_exp_mul_sq_norm_le_of_map_rotation_eq_selfproof · cited by 1
- ProbabilityTheory.Fernique.lintegral_exp_mul_sq_norm_le_mulproof · cited by 1