OAI/Geometry/CylinderCovering/Nilpotent/Cost.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CylinderCovering.Nilpotent.v_nonneg line 13
  2. lemma OAI.CylinderCovering.Nilpotent.a_nonneg line 15
  3. lemma OAI.CylinderCovering.Nilpotent.speedSq_nonneg line 19
  4. lemma OAI.CylinderCovering.Nilpotent.parameter_bounds line 21
  5. lemma OAI.CylinderCovering.Nilpotent.sqrt_denominator_ge_one line 27
  6. lemma OAI.CylinderCovering.Nilpotent.quadraticCoefficient_eq line 33
  7. theorem OAI.CylinderCovering.Nilpotent.integrand_remainder line 38
  8. lemma OAI.CylinderCovering.Nilpotent.continuous_a line 82
  9. lemma OAI.CylinderCovering.Nilpotent.continuous_speedSq line 84
  10. lemma OAI.CylinderCovering.Nilpotent.continuous_quadraticCoefficient line 86
  11. lemma OAI.CylinderCovering.Nilpotent.continuous_integrand line 90
  12. theorem OAI.CylinderCovering.Nilpotent.integral_a line 98
  13. theorem OAI.CylinderCovering.Nilpotent.integral_speedSq line 108
  14. theorem OAI.CylinderCovering.Nilpotent.integral_quadraticCoefficient line 120
  15. theorem OAI.CylinderCovering.Nilpotent.integral_quadraticApproximation line 130
  16. theorem OAI.CylinderCovering.Nilpotent.integral_remainder line 140
  17. theorem OAI.CylinderCovering.Nilpotent.integral_lt_quarter line 160
  18. theorem OAI.CylinderCovering.Nilpotent.integral_expansion line 167
  19. theorem OAI.CylinderCovering.Nilpotent.eventually_integral_lt_quarter line 178
  20. theorem OAI.CylinderCovering.Nilpotent.costSaving_result line 185