OAI/Probability/SKRatio/Quantization/BinGeometry.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKRatio.Bins.sum line 12
  2. def OAI.SKRatio.Bins.overlap line 15
  3. def OAI.SKRatio.Bins.ZeroSum line 18
  4. lemma OAI.SKRatio.Bins.sum_fibers line 20
  5. lemma OAI.SKRatio.Bins.sum_weighted line 26
  6. lemma OAI.SKRatio.Bins.zero_sum_weighted line 38
  7. lemma OAI.SKRatio.Bins.zero_sum_bilinear line 43
  8. lemma OAI.SKRatio.Bins.overlap_symm line 52
  9. lemma OAI.SKRatio.Bins.overlap_self_nonneg line 57
  10. lemma OAI.SKRatio.Bins.overlap_le line 61
  11. lemma OAI.SKRatio.Bins.overlap_abs_le line 77
  12. lemma OAI.SKRatio.Bins.overlap_product_bound line 91
  13. lemma OAI.SKRatio.Bins.double_weighted line 95
  14. lemma OAI.SKRatio.Bins.sum_overlap line 101