OAI/Geometry/CubicTorus/Estimates/BVMovingTrappedDecay.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CubicTorus.MovingCenter.isMinimizerAt_trapped_sequential_decay line 16
2. theorem OAI.CubicTorus.MovingCenter.isMinimizerAt_trapping_subsequence line 106
3. theorem OAI.CubicTorus.MovingCenter.isMinimizerAt_actual_sequential_decay line 165
4. lemma OAI.CubicTorus.MovingCenter.spatial_tilt_closedBall_le_oriented line 211
5. theorem OAI.CubicTorus.MovingCenter.isMinimizerAt_epsilon_improvement line 260
6. theorem OAI.CubicTorus.MovingCenter.isMinimizerAt_excess_contraction line 321
7. theorem OAI.CubicTorus.MovingCenter.isMinimizerAt_uniform_tilt_iteration line 363
8. lemma OAI.CubicTorus.polar_tilt_triangle line 417
9. lemma OAI.CubicTorus.iterated_tilt_limit_excess line 438
10. lemma OAI.CubicTorus.iterated_tilt_limit_oscillation line 500
11. lemma OAI.CubicTorus.iterated_tilt_boundary_cone line 522
12. lemma OAI.CubicTorus.cone_change_normal line 553
13. lemma OAI.CubicTorus.iterated_tilt_limit_excess_tendsto line 579
14. lemma OAI.CubicTorus.iterated_tilt_limit_oscillation_tendsto line 620
15. lemma OAI.CubicTorus.polar_normal_nearby_centers line 659
16. lemma OAI.CubicTorus.continuousOn_of_uniform_normal_tilt line 698
17. lemma OAI.CubicTorus.polar_tilt_limit_two_radius line 726
18. theorem OAI.CubicTorus.MovingCenter.isMinimizerAt_moving_normal_field line 759