OAI/Combinatorics/ThinTrees/HierarchyBounds.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrongThinTree.ShortcutNumeric.eventually_affine_log_lt_rpow line 13
  2. lemma OAI.StrongThinTree.ShortcutNumeric.eventually_const_mul_rpow_le_rpow line 24
  3. lemma OAI.StrongThinTree.ShortcutNumeric.eventually_logb_mul_rpow_lt line 32
  4. def OAI.StrongThinTree.ShortcutNumeric.alpha line 39
  5. def OAI.StrongThinTree.ShortcutNumeric.gamma line 40
  6. def OAI.StrongThinTree.ShortcutNumeric.scale line 41
  7. def OAI.StrongThinTree.ShortcutNumeric.rho line 42
  8. def OAI.StrongThinTree.ShortcutNumeric.count line 43
  9. lemma OAI.StrongThinTree.ShortcutNumeric.bins_log line 45
  10. lemma OAI.StrongThinTree.ShortcutNumeric.eventually_bins_le line 52
  11. lemma OAI.StrongThinTree.ShortcutNumeric.gamma_pos line 69
  12. lemma OAI.StrongThinTree.ShortcutNumeric.scale_pos line 70
  13. lemma OAI.StrongThinTree.ShortcutNumeric.gamma_le_one line 75
  14. lemma OAI.StrongThinTree.ShortcutNumeric.eventually_gamma_lower line 86
  15. lemma OAI.StrongThinTree.ShortcutNumeric.scale_le_alpha line 106
  16. lemma OAI.StrongThinTree.ShortcutNumeric.eventually_scale_lower line 113
  17. lemma OAI.StrongThinTree.ShortcutNumeric.count_pos line 128
  18. lemma OAI.StrongThinTree.ShortcutNumeric.count_upper line 131
  19. lemma OAI.StrongThinTree.ShortcutNumeric.eventually_small line 137
  20. lemma OAI.StrongThinTree.ShortcutNumeric.eventually_assignment line 150
  21. lemma OAI.StrongThinTree.ShortcutNumeric.eventually_log_count_left line 162
  22. lemma OAI.StrongThinTree.ShortcutNumeric.eventually_log_count_right line 186
  23. def OAI.StrongThinTree.ShortcutNumeric.coefficient line 216
  24. def OAI.StrongThinTree.ShortcutNumeric.largeConstant line 220
  25. lemma OAI.StrongThinTree.ShortcutNumeric.coefficient_eq line 222
  26. lemma OAI.StrongThinTree.ShortcutNumeric.eventually_denominator_lower line 229
  27. lemma OAI.StrongThinTree.ShortcutNumeric.eventually_coefficient_bound line 243
  28. lemma OAI.StrongThinTree.ShortcutNumeric.eventually_coefficient_small line 263
  29. lemma OAI.StrongThinTree.ShortcutNumeric.eventually_rho_small line 271
  30. structure OAI.StrongThinTree.ShortcutNumeric.GoodParameters line 278
  31. lemma OAI.StrongThinTree.ShortcutNumeric.eventually_good line 287
  32. lemma OAI.StrongThinTree.ShortcutNumeric.exists_cutoff line 293
  33. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.edgeConnected_of_locally line 306
  34. theorem OAI.StrongThinTree.MultiGraph.Hierarchy.polynomial_shortcut line 313