OAI/Geometry/UnitDistances/Powers.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarUnitDistances.PowerGrowth.Lower line 8
  2. def OAI.PlanarUnitDistances.PowerGrowth.Upper line 11
  3. lemma OAI.PlanarUnitDistances.PowerGrowth.Lower.mono line 16
  4. lemma OAI.PlanarUnitDistances.PowerGrowth.Upper.mono line 21
  5. lemma OAI.PlanarUnitDistances.PowerGrowth.Lower.congr line 26
  6. lemma OAI.PlanarUnitDistances.PowerGrowth.Upper.congr line 29
  7. lemma OAI.PlanarUnitDistances.PowerGrowth.eventually_one_le line 32
  8. lemma OAI.PlanarUnitDistances.PowerGrowth.eventually_base_pos line 35
  9. lemma OAI.PlanarUnitDistances.PowerGrowth.Lower.exponent_mono line 38
  10. lemma OAI.PlanarUnitDistances.PowerGrowth.Upper.exponent_mono line 44
  11. lemma OAI.PlanarUnitDistances.PowerGrowth.Lower.eventually_pos line 50
  12. lemma OAI.PlanarUnitDistances.PowerGrowth.Lower.mul line 55
  13. lemma OAI.PlanarUnitDistances.PowerGrowth.Upper.mul line 64
  14. lemma OAI.PlanarUnitDistances.PowerGrowth.eventually_constant_le_rpow line 74
  15. lemma OAI.PlanarUnitDistances.PowerGrowth.Lower.const_mul line 78
  16. lemma OAI.PlanarUnitDistances.PowerGrowth.Upper.const_mul line 93
  17. lemma OAI.PlanarUnitDistances.PowerGrowth.Upper.add line 104
  18. lemma OAI.PlanarUnitDistances.PowerGrowth.Lower.div line 113
  19. lemma OAI.PlanarUnitDistances.PowerGrowth.Lower.tendsto_atTop line 123
  20. lemma OAI.PlanarUnitDistances.PowerGrowth.not_lower_of_upper_lt line 129
  21. lemma OAI.PlanarUnitDistances.PowerGrowth.upper_rpow line 144
  22. lemma OAI.PlanarUnitDistances.PowerGrowth.lower_rpow line 149
  23. lemma OAI.PlanarUnitDistances.PowerGrowth.upper_const line 154
  24. lemma OAI.PlanarUnitDistances.PowerGrowth.lower_const line 157
  25. lemma OAI.PlanarUnitDistances.PowerGrowth.Upper.div line 161
  26. lemma OAI.PlanarUnitDistances.PowerGrowth.Upper.rpow line 171
  27. lemma OAI.PlanarUnitDistances.PowerGrowth.Lower.rpow line 182
  28. lemma OAI.PlanarUnitDistances.PowerGrowth.Upper.tendsto_zero line 192
  29. lemma OAI.PlanarUnitDistances.PowerGrowth.Upper.ratio_zero line 202
  30. lemma OAI.PlanarUnitDistances.PowerGrowth.upper_log line 209
  31. lemma OAI.PlanarUnitDistances.PowerGrowth.Upper.log line 216
  32. lemma OAI.PlanarUnitDistances.PowerGrowth.Lower.of_loss line 223
  33. lemma OAI.PlanarUnitDistances.PowerGrowth.diagonal line 233
  34. lemma OAI.PlanarUnitDistances.unordered_le_incidences line 247
  35. theorem OAI.PlanarUnitDistances.counterexample_power_sequence line 259
  36. lemma OAI.PlanarUnitDistances.CuttingAsymptotics.cuttingLog_upper line 312
  37. theorem OAI.PlanarUnitDistances.CuttingAsymptotics.exists_cut_sequence line 327
  38. lemma OAI.PlanarUnitDistances.CircleIncidence.high_degree_card line 415
  39. lemma OAI.PlanarUnitDistances.CircleIncidence.incidence_bound_enlarged line 424
  40. theorem OAI.PlanarUnitDistances.CircleIncidence.exists_trimmed line 442
  41. lemma OAI.PlanarUnitDistances.CuttingAsymptotics.incidence_upper line 487
  42. theorem OAI.PlanarUnitDistances.CuttingAsymptotics.trim_sequence line 515