OAI/Geometry/Cannon/Boundary/VisualScale.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CannonGraph.product2_base_upper line 22
  2. lemma OAI.CannonGraph.product2_replace_endpoints line 30
  3. lemma OAI.CannonGraph.product2_base_cross line 42
  4. lemma OAI.CannonRelease.product2_mul line 69
  5. lemma OAI.CannonRelease.product2_ray_bounded line 75
  6. lemma OAI.CannonRelease.translated_mixed_product_large line 84
  7. lemma OAI.CannonRelease.translated_product_independent_error line 105
  8. lemma OAI.CannonRelease.translated_product2_cross line 146
  9. lemma OAI.CannonRelease.translated_preDist_crossratio line 157
  10. lemma OAI.CannonReal.mul_four_le line 212
  11. theorem OAI.CannonRelease.boundary_uniform_cross_bound line 230
  12. lemma OAI.CannonGraph.product2_prefix line 278
  13. lemma OAI.CannonGraph.product2_base_change line 303
  14. lemma OAI.CannonRelease.expansion_product_sums line 323
  15. lemma OAI.CannonReal.exp_neg_nat_min line 357
  16. lemma OAI.CannonReal.exp_expansion line 368
  17. def OAI.CannonVisual.visualScale line 391
  18. lemma OAI.CannonVisual.visualScale_pos line 392
  19. lemma OAI.CannonRelease.preDist_expansion line 404
  20. lemma OAI.CannonReal.max_le_twice_max line 441
  21. lemma OAI.CannonReal.mul_three_le line 448
  22. theorem OAI.CannonRelease.visual_expansion_ray line 463
  23. lemma OAI.CannonGraph.product2_replace_one line 519
  24. lemma OAI.CannonGraph.product2_complement line 530
  25. lemma OAI.CannonGraph.vertex_close_to_ray line 537
  26. theorem OAI.CannonRelease.coarse_prefix_of_distinct_rays line 583
  27. lemma OAI.CannonVisual.visualScale_eq_pow line 620
  28. lemma OAI.CannonVisual.visualScale_near line 628
  29. lemma OAI.CannonVisual.visualScale_tendsto_zero line 644