OAI/Probability/SKRatio/Quantization/BinParameters.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKRatio.Bins.count line 13
  2. def OAI.SKRatio.Bins.binMean line 15
  3. def OAI.SKRatio.Bins.binCentered line 17
  4. lemma OAI.SKRatio.Bins.sum_const_bin line 19
  5. lemma OAI.SKRatio.Bins.sum_add_bin line 26
  6. lemma OAI.SKRatio.Bins.sum_sub_bin line 28
  7. lemma OAI.SKRatio.Bins.count_mul_binMean line 31
  8. lemma OAI.SKRatio.Bins.binCentered_zeroSum line 38
  9. lemma OAI.SKRatio.Bins.binCentered_decomp line 43
  10. lemma OAI.SKRatio.Bins.bin_orthogonal_decomposition line 46
  11. lemma OAI.SKRatio.Bins.centered_fiber_sq line 65
  12. lemma OAI.SKRatio.Bins.normalized_fiber_sq line 73
  13. abbrev OAI.SKRatio.Bins.ParameterSpace line 81
  14. def OAI.SKRatio.Bins.ParameterSet line 83
  15. abbrev OAI.SKRatio.Bins.Parameters line 86
  16. lemma OAI.SKRatio.Bins.parameterSet_compact line 89
  17. instance OAI.SKRatio.Bins.(instance at line 98) line 98
  18. def OAI.SKRatio.Bins.paramB line 100
  19. def OAI.SKRatio.Bins.paramR line 101
  20. lemma OAI.SKRatio.Bins.paramR_nonneg line 104
  21. lemma OAI.SKRatio.Bins.param_sum_sq line 107
  22. def OAI.SKRatio.Bins.parametersOf line 112
  23. lemma OAI.SKRatio.Bins.parametersOf_B line 126
  24. lemma OAI.SKRatio.Bins.parametersOf_R line 128
  25. theorem OAI.SKRatio.Bins.parameters_finite_net line 132