OAI/Probability/StrongRayleigh/ElementaryResponse.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem336AdditiveD139.boolReal_nonneg line 12
2. lemma OAI.Problem336AdditiveD139.boolReal_le_one line 13
3. lemma OAI.Problem336AdditiveD139.boolReal_mul_self line 14
4. lemma OAI.Problem336AdditiveD139.tiltMean_nonneg line 17
5. lemma OAI.Problem336AdditiveD139.tiltMean_le_one line 27
6. lemma OAI.Problem336AdditiveD139.tiltSecondMoment_self line 38
7. lemma OAI.Problem336AdditiveD139.tiltCovariance_self line 44
8. lemma OAI.Problem336AdditiveD139.tiltCovariance_self_nonneg line 50
9. lemma OAI.Problem336AdditiveD139.twice_tilt_variance_le_half line 56