OAI/Geometry/Cannon/Energy/PathCosts.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CannonPotential.pathCosts line 29
  2. def OAI.CannonPotential.distanceFrom line 32
  3. lemma OAI.CannonPotential.pathCosts_nonempty line 34
  4. lemma OAI.CannonPotential.pathCosts_bddBelow line 43
  5. lemma OAI.CannonPotential.distanceFrom_nonneg line 48
  6. lemma OAI.CannonPotential.distanceFrom_le_path line 55
  7. lemma OAI.CannonPotential.distanceFrom_triangle line 59
  8. def OAI.CannonPotential.raw line 71
  9. lemma OAI.CannonPotential.raw_on_top line 76
  10. lemma OAI.CannonPotential.raw_bounds line 80
  11. lemma OAI.CannonPotential.raw_le_add_cost line 87
  12. theorem OAI.CannonPotential.raw_path_variation line 106
  13. lemma OAI.CannonPotential.raw_on_bottom line 114
  14. lemma OAI.CannonBands.last_level_suffix line 135
  15. lemma OAI.CannonBands.value_le_cost_of_top line 150
  16. theorem OAI.CannonBands.extended_path_variation line 192
  17. abbrev OAI.CannonBands.Strip line 264
  18. def OAI.CannonBands.extend line 266
  19. lemma OAI.CannonBands.extend_on_strip line 271
  20. lemma OAI.CannonBands.extend_bounds line 276
  21. lemma OAI.CannonBands.extend_top line 285
  22. lemma OAI.CannonBands.extend_bottom line 295
  23. lemma OAI.CannonBands.cost_preimage_image line 305
  24. def OAI.CannonBands.stripPath line 317
  25. lemma OAI.CannonBands.stripPath_image_range line 325
  26. def OAI.CannonBands.rawExtended line 331
  27. theorem OAI.CannonBands.rawExtended_properties line 335
  28. abbrev OAI.CannonBands.ChartSquare line 387
  29. def OAI.CannonBands.height line 389
  30. def OAI.CannonBands.stripHomeomorph line 391
  31. lemma OAI.CannonBands.strip_pathConnected line 401
  32. lemma OAI.CannonBands.strip_top_nonempty line 410