OAI/Probability/SKRatio/Quantization/BinDirections.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKRatio.Bins.sum_scale_bin line 13
  2. lemma OAI.SKRatio.Bins.zeroSum_scale_bin line 22
  3. lemma OAI.SKRatio.Bins.overlap_scale_bin line 27
  4. def OAI.SKRatio.Bins.DirectionSet line 35
  5. abbrev OAI.SKRatio.Bins.Directions line 38
  6. lemma OAI.SKRatio.Bins.directions_zeroSum line 40
  7. lemma OAI.SKRatio.Bins.directions_overlap line 43
  8. lemma OAI.SKRatio.Bins.directions_norm_sq line 48
  9. lemma OAI.SKRatio.Bins.directionSet_closed line 55
  10. lemma OAI.SKRatio.Bins.directionSet_compact line 64
  11. instance OAI.SKRatio.Bins.(instance at line 72) line 72
  12. lemma OAI.SKRatio.Bins.two_sites_of_count line 75
  13. lemma OAI.SKRatio.Bins.directions_nonempty line 81
  14. def OAI.SKRatio.Bins.vectorOf line 109
  15. lemma OAI.SKRatio.Bins.vectorOf_unit line 112
  16. lemma OAI.SKRatio.Bins.vectorOf_continuous line 125
  17. lemma OAI.SKRatio.Bins.scaled_directions_continuous line 131
  18. lemma OAI.SKRatio.Bins.vectorOf_difference line 137
  19. lemma OAI.SKRatio.Bins.fiber_sq_le line 163
  20. lemma OAI.SKRatio.Bins.fiber_zero_of_sqrt_zero line 170
  21. theorem OAI.SKRatio.Bins.vectorOf_surjective line 178