OAI/Probability/SKRatio/Variational/ScalarVariance.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKRatio.Scalar.l2Norm_add line 15
2. lemma OAI.SKRatio.Scalar.l2Norm_const_mul line 24
3. lemma OAI.SKRatio.Scalar.sd_sq line 34
4. lemma OAI.SKRatio.Scalar.sd_sq_eq line 36
5. lemma OAI.SKRatio.Scalar.square_center_expansion line 41
6. lemma OAI.SKRatio.Scalar.sd_min_center line 49
7. lemma OAI.SKRatio.Scalar.centered_add line 55
8. lemma OAI.SKRatio.Scalar.centered_const_mul line 62
9. lemma OAI.SKRatio.Scalar.centered_sub_const line 68
10. lemma OAI.SKRatio.Scalar.sd_add line 75
11. lemma OAI.SKRatio.Scalar.sd_const_mul line 82
12. lemma OAI.SKRatio.Scalar.sd_sub_const line 87
13. lemma OAI.SKRatio.Scalar.sd_sub line 92
14. lemma OAI.SKRatio.Scalar.abs_sd_sub_le line 99
15. lemma OAI.SKRatio.Scalar.sd_mono_measure line 108
16. lemma OAI.SKRatio.Scalar.sd_mono_measure_sqrt line 121
17. lemma OAI.SKRatio.Scalar.weighted_sd_mono_measure line 129
18. lemma OAI.SKRatio.Scalar.weighted_sd_temperature_mono line 146
19. lemma OAI.SKRatio.Scalar.weighted_sd_temperature_mono' line 152
20. lemma OAI.SKRatio.Scalar.weighted_mv_temperature_mono line 159
21. lemma OAI.SKRatio.Scalar.weighted_R_temperature_mono line 171