OAI/Probability/SKRatio/Variational/ScalarMoments.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKRatio.Scalar.variance line 14
2. lemma OAI.SKRatio.Scalar.variance_coe line 16
3. def OAI.SKRatio.Scalar.fieldLaw line 19
4. instance OAI.SKRatio.Scalar.(instance at line 20) line 20
5. lemma OAI.SKRatio.Scalar.memLp_m line 24
6. lemma OAI.SKRatio.Scalar.memLp_v line 28
7. lemma OAI.SKRatio.Scalar.memLp_mv line 32
8. lemma OAI.SKRatio.Scalar.tilted_integral line 42
9. lemma OAI.SKRatio.Scalar.centered_gaussian_integral_neg line 51
10. lemma OAI.SKRatio.Scalar.tilted_odd_integrand line 57
11. theorem OAI.SKRatio.Scalar.sign_identity line 66
12. lemma OAI.SKRatio.Scalar.mean_m_eq_mean_m_sq line 98
13. lemma OAI.SKRatio.Scalar.mean_mv_eq_mean_m_sq_v line 103
14. lemma OAI.SKRatio.Scalar.mean_mv_nonneg line 111
15. lemma OAI.SKRatio.Scalar.memLp_field line 115
16. lemma OAI.SKRatio.Scalar.memLp_field_v line 118
17. lemma OAI.SKRatio.Scalar.v_hasDerivAt line 127
18. theorem OAI.SKRatio.Scalar.field_variance_identity line 132
19. def OAI.SKRatio.Scalar.multiplier line 167
20. lemma OAI.SKRatio.Scalar.multiplier_pos line 169
21. lemma OAI.SKRatio.Scalar.multiplier_le line 173
22. lemma OAI.SKRatio.Scalar.continuous_multiplier line 180
23. lemma OAI.SKRatio.Scalar.mean_multiplier line 184