OAI/Geometry/LatticeCovering/Lines.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SingleLatticeCovering.Folded.gridMass_eq_usableMass line 41
  2. lemma OAI.SingleLatticeCovering.Folded.probability_eq_bitMass line 51
  3. lemma OAI.SingleLatticeCovering.Folded.wordMass_eq_productMass line 58
  4. lemma OAI.SingleLatticeCovering.Folded.mean_fairRate_lower line 65
  5. lemma OAI.SingleLatticeCovering.Folded.eligible_window line 87
  6. lemma OAI.SingleLatticeCovering.Folded.eventually_previous_cap line 104
  7. lemma OAI.SingleLatticeCovering.Folded.eventually_line_collision line 113
  8. lemma OAI.SingleLatticeCovering.Folded.window_line_choice line 124
  9. lemma OAI.SingleLatticeCovering.Folded.line_mean_error line 151
  10. lemma OAI.SingleLatticeCovering.Folded.usable_mass_error line 159
  11. lemma OAI.SingleLatticeCovering.Folded.sampler_factor_lower line 171
  12. def OAI.SingleLatticeCovering.Folded.eligible line 187
  13. def OAI.SingleLatticeCovering.Folded.anchorWeight line 190
  14. def OAI.SingleLatticeCovering.Folded.blockFunction line 192
  15. theorem OAI.SingleLatticeCovering.Folded.eventually_usable_gaussian line 199
  16. def OAI.SingleLatticeCovering.Folded.balanced line 287
  17. lemma OAI.SingleLatticeCovering.Folded.balanced_probability line 290
  18. lemma OAI.SingleLatticeCovering.Folded.window_atom line 297
  19. lemma OAI.SingleLatticeCovering.Folded.eventually_atom_exponent line 316
  20. theorem OAI.SingleLatticeCovering.Folded.atom_decay line 335
  21. lemma OAI.SingleLatticeCovering.ConstructionA.anchor_mem_cube line 375
  22. lemma OAI.SingleLatticeCovering.ConstructionA.lineMax_anchor line 384
  23. theorem OAI.SingleLatticeCovering.ConstructionA.gaussian_cell line 405
  24. theorem OAI.SingleLatticeCovering.Folded.eventually_eligible_atom line 460
  25. lemma OAI.SingleLatticeCovering.Folded.eventually_logMean_height_le line 512
  26. lemma OAI.SingleLatticeCovering.Folded.group_log_bound line 531
  27. def OAI.SingleLatticeCovering.Vertical.join line 568
  28. lemma OAI.SingleLatticeCovering.Vertical.mem_join line 572
  29. lemma OAI.SingleLatticeCovering.Vertical.sum_join line 582
  30. theorem OAI.SingleLatticeCovering.Vertical.weighted_join line 601
  31. lemma OAI.SingleLatticeCovering.Vertical.join_subset_product line 632
  32. def OAI.SingleLatticeCovering.Vertical.SuffixBinary line 641
  33. def OAI.SingleLatticeCovering.Vertical.bits line 645
  34. lemma OAI.SingleLatticeCovering.Vertical.bits_injective line 648
  35. lemma OAI.SingleLatticeCovering.Vertical.bits_scalar line 655