OAI/Probability/SKRatio/Quantization/BinFunctional.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKRatio.Bins.binT line 15
  2. lemma OAI.SKRatio.Bins.sum_count line 18
  3. lemma OAI.SKRatio.Bins.binT_nonneg line 23
  4. lemma OAI.SKRatio.Bins.binT_sq line 26
  5. lemma OAI.SKRatio.Bins.binT_unit line 30
  6. lemma OAI.SKRatio.Bins.sqrt_count_mul_div line 35
  7. lemma OAI.SKRatio.Bins.vectorOf_sum line 42
  8. lemma OAI.SKRatio.Bins.vectorOf_sq_sum line 51
  9. def OAI.SKRatio.Bins.moment line 61
  10. lemma OAI.SKRatio.Bins.vectorOf_moment line 64
  11. def OAI.SKRatio.Bins.finiteRadicalSq line 74
  12. def OAI.SKRatio.Bins.finiteGaussian line 78
  13. lemma OAI.SKRatio.Bins.binVariance_normalized line 82
  14. lemma OAI.SKRatio.Bins.radicalSq_normalized line 117
  15. theorem OAI.SKRatio.Bins.normalized_projected_tail line 126
  16. def OAI.SKRatio.Bins.finiteA line 160
  17. def OAI.SKRatio.Bins.finiteV line 169
  18. lemma OAI.SKRatio.Bins.continuous_paramB line 174
  19. lemma OAI.SKRatio.Bins.continuous_paramR line 176
  20. lemma OAI.SKRatio.Bins.continuous_moment line 179
  21. lemma OAI.SKRatio.Bins.continuous_finiteRadicalSq line 184
  22. lemma OAI.SKRatio.Bins.continuous_finiteGaussian line 191
  23. lemma OAI.SKRatio.Bins.continuous_finiteA line 201
  24. lemma OAI.SKRatio.Bins.continuous_finiteV line 208