OAI/Geometry/CylinderCovering/Caps/FiniteAsymptotics.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CylinderCovering.HalfheightFinite.height_pos line 11
  2. theorem OAI.CylinderCovering.HalfheightFinite.limitingArea_eq_Q line 15
  3. theorem OAI.CylinderCovering.HalfheightFinite.cubic_cap_dictionary line 36
  4. theorem OAI.CylinderCovering.HalfheightFinite.fractional_power_dictionary line 41
  5. theorem OAI.CylinderCovering.HalfheightFinite.fractional_cap_dictionary line 49
  6. theorem OAI.CylinderCovering.HalfheightFinite.limitingArea_cubic_eq_Q line 56
  7. theorem OAI.CylinderCovering.HalfheightFinite.limitingArea_fractional_eq_Q line 64
  8. theorem OAI.CylinderCovering.HalfheightFinite.half_tendsto_right line 73
  9. theorem OAI.CylinderCovering.HalfheightFinite.cubic_cost_bigO line 83
  10. theorem OAI.CylinderCovering.HalfheightFinite.fractional_cost_bigO line 98
  11. theorem OAI.CylinderCovering.HalfheightFinite.limiting_costs_strict line 121
  12. theorem OAI.CylinderCovering.HalfheightFinite.finite_saving_of_convergence line 136
  13. theorem OAI.CylinderCovering.HalfheightFinite.eventual_finite_saving line 142