OAI/Geometry/UnitDistances/AbsoluteValues.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarUnitDistances.WeightedAbsoluteValues.badPrimes line 12
  2. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.padic_nat_eq line 14
  3. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.prod_padic_nat line 21
  4. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.padic_int_natAbs line 39
  5. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.padic_rat_outside line 46
  6. theorem OAI.PlanarUnitDistances.WeightedAbsoluteValues.rational_product_formula line 60
  7. def OAI.PlanarUnitDistances.WeightedAbsoluteValues.primeEmbedding line 93
  8. def OAI.PlanarUnitDistances.WeightedAbsoluteValues.primeAbsoluteValue line 96
  9. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.primeAbsoluteValue_apply line 99
  10. theorem OAI.PlanarUnitDistances.WeightedAbsoluteValues.primeAbsoluteValue_rat line 102
  11. theorem OAI.PlanarUnitDistances.WeightedAbsoluteValues.primeAbsoluteValue_nonarch line 109
  12. def OAI.PlanarUnitDistances.WeightedAbsoluteValues.finiteEntry line 116
  13. def OAI.PlanarUnitDistances.WeightedAbsoluteValues.infiniteEntry line 120
  14. theorem OAI.PlanarUnitDistances.WeightedAbsoluteValues.infiniteEntry_apply line 123
  15. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.infiniteEntry_count line 126
  16. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.finiteEntry_nonarch line 129
  17. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.finiteEntry_rat line 137
  18. def OAI.PlanarUnitDistances.WeightedAbsoluteValues.rootDenominators line 143
  19. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.nonarch_root_one line 148
  20. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.finiteEntry_le_one_off_denominators line 174
  21. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.finiteEntry_eq_one_off_support line 201
  22. theorem OAI.PlanarUnitDistances.WeightedAbsoluteValues.finiteEntry_hasFiniteMulSupport line 212
  23. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.finiteEntry_block line 229
  24. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.infiniteEntry_block line 236
  25. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.rational_product_formula_on line 242
  26. theorem OAI.PlanarUnitDistances.WeightedAbsoluteValues.product_formula line 268
  27. theorem OAI.PlanarUnitDistances.WeightedAbsoluteValues.weighted_log_product_formula line 298
  28. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.finiteEntry_composed_support line 327
  29. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.finite_posLog_support line 342
  30. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.finite_log_support line 347
  31. def OAI.PlanarUnitDistances.WeightedAbsoluteValues.exactHeight line 351
  32. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.finrank_pos line 357
  33. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.exactHeight_nonneg line 361
  34. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.exactHeight_zero line 367
  35. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.exactHeight_one line 371
  36. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.exactHeight_neg line 375
  37. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.exactHeight_inv line 378
  38. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.exactHeight_mul_le line 405
  39. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.exactHeight_add_le line 432
  40. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.abs_log_eq_posLog_add line 468
  41. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.weighted_abs_log_eq_twice line 473
  42. theorem OAI.PlanarUnitDistances.ExactHeightLocal.abv_root_le line 503
  43. theorem OAI.PlanarUnitDistances.ExactHeightLocal.nonarch_root_le line 534
  44. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.posLog_max_one line 574
  45. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.local_posLog_root line 580
  46. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.local_nonarch_posLog_root line 594
  47. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.exactHeight_root_le line 604