OAI/Probability/SKRatio/Quantization/BinProcess.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKRatio.Bins.average line 15
2. def OAI.SKRatio.Bins.centered line 16
3. lemma OAI.SKRatio.Bins.average_add line 19
4. lemma OAI.SKRatio.Bins.average_mul line 22
5. lemma OAI.SKRatio.Bins.average_const line 24
6. lemma OAI.SKRatio.Bins.average_zeroSum line 28
7. lemma OAI.SKRatio.Bins.centered_sq line 32
8. lemma OAI.SKRatio.Bins.centered_sq_le line 42
9. def OAI.SKRatio.Bins.fullCoeff line 46
10. lemma OAI.SKRatio.Bins.continuous_centered line 52
11. lemma OAI.SKRatio.Bins.continuous_fullCoeff line 58
12. def OAI.SKRatio.Bins.crossCoeff line 72
13. lemma OAI.SKRatio.Bins.crossCoeff_eq line 76
14. lemma OAI.SKRatio.Bins.centered_add_zeroSum line 86
15. lemma OAI.SKRatio.Bins.zeroSum_mul line 93
16. lemma OAI.SKRatio.Bins.fullCoeff_decomposition line 106
17. lemma OAI.SKRatio.Bins.fullCoeff_sq_le line 123
18. lemma OAI.SKRatio.Bins.fullCoeff_norm_le line 157
19. lemma OAI.SKRatio.Bins.gaussianSup_add_common line 172
20. lemma OAI.SKRatio.Bins.integral_gaussianSup_add_common line 189
21. theorem OAI.SKRatio.Bins.full_sup_expectation_le line 208
22. theorem OAI.SKRatio.Bins.full_sup_lipschitz line 224
23. theorem OAI.SKRatio.Bins.full_sup_tail line 234