OAI/Probability/SKRatio/Quantization/IntervalBins.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKRatio.Bins.intervalBin line 16
  2. lemma OAI.SKRatio.Bins.intervalBin_le_cut line 21
  3. lemma OAI.SKRatio.Bins.intervalBin_eq_zero line 41
  4. lemma OAI.SKRatio.Bins.intervalBin_eq_last line 46
  5. lemma OAI.SKRatio.Bins.intervalBin_eq_middle line 58
  6. lemma OAI.SKRatio.Bins.measurableSet_intervalBin line 75
  7. lemma OAI.SKRatio.Bins.measurable_intervalBin line 90
  8. lemma OAI.SKRatio.Bins.intervalBin_empirical line 96
  9. lemma OAI.SKRatio.Bins.gaussianReal_real_pos_of_volume_pos line 120
  10. lemma OAI.SKRatio.Bins.intervalBin_mass_pos line 125