OAI/Geometry/UnitDistances/SmallHeight.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UnitDistances.ExactHeightObstruction.height line 8
  2. lemma OAI.UnitDistances.ExactHeightObstruction.height_nonneg line 10
  3. lemma OAI.UnitDistances.ExactHeightObstruction.height_zero line 12
  4. lemma OAI.UnitDistances.ExactHeightObstruction.height_one line 14
  5. lemma OAI.UnitDistances.ExactHeightObstruction.height_neg line 16
  6. lemma OAI.UnitDistances.ExactHeightObstruction.height_inv line 17
  7. lemma OAI.UnitDistances.ExactHeightObstruction.height_mul_le line 19
  8. lemma OAI.UnitDistances.ExactHeightObstruction.height_add_le line 20
  9. lemma OAI.UnitDistances.ExactHeightObstruction.height_root_le line 22
  10. def OAI.UnitDistances.ExactSmallHeightField.Negligible line 35
  11. theorem OAI.UnitDistances.ExactSmallHeightField.Negligible.congr line 41
  12. theorem OAI.UnitDistances.ExactSmallHeightField.Negligible.zero line 48
  13. theorem OAI.UnitDistances.ExactSmallHeightField.Negligible.one line 52
  14. theorem OAI.UnitDistances.ExactSmallHeightField.Negligible.neg line 56
  15. theorem OAI.UnitDistances.ExactSmallHeightField.Negligible.inv line 59
  16. theorem OAI.UnitDistances.ExactSmallHeightField.Negligible.mul line 63
  17. theorem OAI.UnitDistances.ExactSmallHeightField.Negligible.add line 75
  18. def OAI.UnitDistances.ExactSmallHeightField.constants line 89
  19. theorem OAI.UnitDistances.ExactSmallHeightField.mk_mem_constants_iff line 106
  20. theorem OAI.UnitDistances.ExactSmallHeightField.Negligible.root line 115
  21. theorem OAI.UnitDistances.ExactSmallHeightField.root_mem_constants line 132
  22. theorem OAI.UnitDistances.ExactSmallHeightField.algebraic_mem_constants line 146
  23. theorem OAI.UnitDistances.ExactSmallHeightField.large_height_transcendental line 162
  24. def OAI.UnitDistances.UltraField.map line 181
  25. lemma OAI.UnitDistances.UltraField.map_mk line 190
  26. lemma OAI.UnitDistances.UltraField.transcendental_map line 193
  27. def OAI.PlanarUnitDistances.UltraHeightGrid.complexMap line 212
  28. def OAI.PlanarUnitDistances.UltraHeightGrid.complexAlgebra line 215
  29. lemma OAI.PlanarUnitDistances.UltraHeightGrid.negligible_of_bound line 220
  30. lemma OAI.PlanarUnitDistances.UltraHeightGrid.large_transcendental line 235
  31. lemma OAI.PlanarUnitDistances.UltraHeightGrid.rectangle_constant line 242
  32. def OAI.PlanarUnitDistances.EdgeLabels.label line 275
  33. lemma OAI.PlanarUnitDistances.EdgeLabels.transcendental line 279
  34. lemma OAI.PlanarUnitDistances.EdgeLabels.rectangle line 285
  35. lemma OAI.PlanarUnitDistances.EdgeLabels.distance line 298
  36. lemma OAI.UnitDistances.GridCount.pow_expect_le line 314
  37. lemma OAI.UnitDistances.GridCount.expect_prod_tuple line 324
  38. theorem OAI.UnitDistances.GridCount.complete_grid_density line 330
  39. lemma OAI.UnitDistances.GridCount.expect_pair_indicator line 364
  40. def OAI.UnitDistances.GridCount.grids line 374
  41. theorem OAI.UnitDistances.GridCount.complete_grid_count line 378
  42. theorem OAI.UnitDistances.GenericDiagonal.exists_avoiding line 399
  43. theorem OAI.UnitDistances.GenericDiagonal.diagonal_nat line 410
  44. theorem OAI.UnitDistances.GenericDiagonal.diagonal_countable line 435
  45. lemma OAI.PlanarUnitDistances.PowerGrowth.Lower.one line 466
  46. lemma OAI.PlanarUnitDistances.PowerGrowth.Upper.one line 471
  47. lemma OAI.PlanarUnitDistances.PowerGrowth.Lower.pow line 476
  48. lemma OAI.PlanarUnitDistances.PowerGrowth.Upper.pow line 483
  49. lemma OAI.PlanarUnitDistances.PowerGrowth.eventually_lt_of_upper_lower line 491
  50. def OAI.PlanarUnitDistances.PowerGrowth.Saving line 497
  51. lemma OAI.PlanarUnitDistances.PowerGrowth.Saving.add line 500
  52. lemma OAI.PlanarUnitDistances.PowerGrowth.Saving.zero line 507
  53. lemma OAI.PlanarUnitDistances.PowerGrowth.Saving.finset_sum line 513
  54. lemma OAI.PlanarUnitDistances.PowerGrowth.Saving.eventually_lt line 524