OAI/Geometry/Cannon/Flows/DyadicBin.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CannonPairs.dyadic_bin line 21
  2. theorem OAI.CannonPairs.probability_pattern_class line 46
  3. lemma OAI.CannonPairs.discarded_weight_bound line 89
  4. theorem OAI.CannonPairs.eventually_probability_class line 134
  5. lemma OAI.CannonPairs.division_difference_tendsto line 197
  6. theorem OAI.CannonPairs.division_geometric_tail line 206
  7. lemma OAI.CannonPairs.division_exp_tail line 224
  8. lemma OAI.CannonPairs.depth_difference_tendsto line 230
  9. lemma OAI.CannonPairs.pair_split_exponent line 242
  10. lemma OAI.CannonPairs.pair_split_ratio line 249
  11. lemma OAI.CannonPairs.pair_overlap_exponential line 252
  12. lemma OAI.CannonApprox.FlowSetup.depth_tendsto line 278
  13. theorem OAI.CannonApprox.FlowSetup.card_exponential line 288
  14. theorem OAI.CannonApprox.FlowSetup.pattern_class line 323
  15. theorem OAI.CannonPairs.ordered_cost_real_multiplicity line 387
  16. theorem OAI.CannonPairs.oriented_cost_real_multiplicity line 427
  17. theorem OAI.CannonPairs.geometric_cost_multiplicity line 448
  18. theorem OAI.CannonPairs.geometric_pair_comparison line 493
  19. theorem OAI.CannonPairs.charged_pair_comparison line 555