OAI/Probability/SKRatio/Quantization/Quantizer.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKRatio.Bins.gridCut line 15
  2. def OAI.SKRatio.Bins.gridRep line 17
  3. def OAI.SKRatio.Bins.gridQuant line 19
  4. lemma OAI.SKRatio.Bins.gridCut_strictMono line 21
  5. lemma OAI.SKRatio.Bins.gridCut_zero line 27
  6. lemma OAI.SKRatio.Bins.gridCut_last line 28
  7. lemma OAI.SKRatio.Bins.gridRep_zero line 31
  8. lemma OAI.SKRatio.Bins.gridRep_last line 32
  9. lemma OAI.SKRatio.Bins.gridRep_middle line 35
  10. lemma OAI.SKRatio.Bins.gridRep_abs_le line 39
  11. lemma OAI.SKRatio.Bins.gridQuant_left line 49
  12. lemma OAI.SKRatio.Bins.gridQuant_right line 56
  13. lemma OAI.SKRatio.Bins.gridQuant_middle line 63
  14. lemma OAI.SKRatio.Bins.gridQuant_square_error line 87
  15. lemma OAI.SKRatio.Bins.measurable_gridQuant line 107
  16. lemma OAI.SKRatio.Bins.gridQuant_compact_error line 111