OAI/Geometry/LatticeCovering/Bits.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SingleLatticeCovering.Bits.groupShift line 35
  2. def OAI.SingleLatticeCovering.Bits.fairAverage line 37
  3. def OAI.SingleLatticeCovering.Bits.biasedAverage line 40
  4. lemma OAI.SingleLatticeCovering.Bits.groupShift_reindex line 43
  5. lemma OAI.SingleLatticeCovering.Bits.fairAverage_reindex line 47
  6. lemma OAI.SingleLatticeCovering.Bits.filled_groupShift line 62
  7. lemma OAI.SingleLatticeCovering.Bits.conditional_shift_average line 72
  8. lemma OAI.SingleLatticeCovering.Bits.sampler_finite_index line 86
  9. def OAI.SingleLatticeCovering.Bits.componentGood line 127
  10. def OAI.SingleLatticeCovering.Bits.badMixture line 131
  11. lemma OAI.SingleLatticeCovering.Bits.badMixture_nonneg line 134
  12. lemma OAI.SingleLatticeCovering.Bits.badMixture_le_one line 142
  13. lemma OAI.SingleLatticeCovering.Bits.component_failure_mean_le line 151
  14. theorem OAI.SingleLatticeCovering.Bits.expected_badMixture_le line 187
  15. theorem OAI.SingleLatticeCovering.Bits.biasedAverage_of_badMixture_le line 218
  16. def OAI.SingleLatticeCovering.WeightedSelection.mass line 244
  17. def OAI.SingleLatticeCovering.WeightedSelection.loss line 246
  18. lemma OAI.SingleLatticeCovering.WeightedSelection.mean_loss_le line 249
  19. theorem OAI.SingleLatticeCovering.WeightedSelection.choose_usable line 263
  20. def OAI.SingleLatticeCovering.Bits.alpha line 312
  21. lemma OAI.SingleLatticeCovering.Bits.alpha_pos line 313
  22. lemma OAI.SingleLatticeCovering.Bits.alpha_le_half line 314
  23. lemma OAI.SingleLatticeCovering.Bits.eventually_mixture_parameters line 321
  24. lemma OAI.SingleLatticeCovering.Bits.expected_badMixture_uniform_le line 336
  25. theorem OAI.SingleLatticeCovering.Bits.usable_anchor_selection line 365
  26. theorem OAI.SingleLatticeCovering.Bits.usable_anchor_selection_uniform line 425
  27. abbrev OAI.SingleLatticeCovering.Blocks.Direction line 497
  28. def OAI.SingleLatticeCovering.Blocks.lineSum line 500
  29. def OAI.SingleLatticeCovering.Blocks.lineMax line 503
  30. lemma OAI.SingleLatticeCovering.Blocks.lineMax_nonneg line 506
  31. lemma OAI.SingleLatticeCovering.Blocks.lineMax_le line 510
  32. lemma OAI.SingleLatticeCovering.Blocks.lineMax_le_sum line 513
  33. lemma OAI.SingleLatticeCovering.Blocks.mean_lineSum line 519
  34. def OAI.SingleLatticeCovering.Blocks.collision line 528
  35. lemma OAI.SingleLatticeCovering.Blocks.collision_of_two line 531
  36. lemma OAI.SingleLatticeCovering.Blocks.line_loss_le_collision line 543
  37. lemma OAI.SingleLatticeCovering.Blocks.direction_point_prob line 578
  38. lemma OAI.SingleLatticeCovering.Blocks.collision_indicator_le line 591
  39. lemma OAI.SingleLatticeCovering.Blocks.collision_probability_le line 618
  40. lemma OAI.SingleLatticeCovering.Blocks.mean_line_loss_le line 636
  41. lemma OAI.SingleLatticeCovering.Blocks.mean_direction_loss_le line 650
  42. theorem OAI.SingleLatticeCovering.Blocks.exists_sparse_line line 683
  43. lemma OAI.SingleLatticeCovering.Blocks.card_direction line 697
  44. lemma OAI.SingleLatticeCovering.Blocks.collision_factor_le_twice line 702
  45. def OAI.SingleLatticeCovering.Blocks.usableMass line 719
  46. def OAI.SingleLatticeCovering.Blocks.sparseWeight line 724
  47. lemma OAI.SingleLatticeCovering.Blocks.mean_sparseWeight line 727
  48. lemma OAI.SingleLatticeCovering.Blocks.usable_density_le line 736
  49. theorem OAI.SingleLatticeCovering.Blocks.gaussian_window_sparse_line line 752