OAI/Geometry/CubicTorus/Regularity/BVFlatBlowupRegular.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.MovingCenter.isMinimizerAt_moving_normal_modulus line 15
  2. def OAI.CubicTorus.blowupTilt line 176
  3. lemma OAI.CubicTorus.continuous_blowupTilt line 179
  4. lemma OAI.CubicTorus.blowupTilt_nonneg line 183
  5. lemma OAI.CubicTorus.blowupTilt_zero line 186
  6. lemma OAI.CubicTorus.blowupTilt_hasCompactSupport line 194
  7. lemma OAI.CubicTorus.flat_normal_tilt_limit line 202
  8. lemma OAI.CubicTorus.spatial_tilt_le_blowupTilt line 224
  9. theorem OAI.CubicTorus.isMinimizerAt_c1_of_flat_normal_blowup line 267
  10. def OAI.CubicTorus.BoundaryNormalChart line 326
  11. lemma OAI.CubicTorus.flat_moving_normal_tilt_limit line 336
  12. theorem OAI.CubicTorus.isMinimizerAt_flat_moving_normal_charts line 358
  13. lemma OAI.CubicTorus.preconnected_crosses_frontier line 414
  14. lemma OAI.CubicTorus.isMinimizerAt_two_phase_frontier_in_ball line 432
  15. theorem OAI.CubicTorus.isMinimizerAt_moving_frontier_approximation line 455
  16. theorem OAI.CubicTorus.isMinimizerAt_flat_moving_graphs line 507
  17. theorem OAI.CubicTorus.actual_secondary_graph_approximants line 595
  18. theorem OAI.CubicTorus.isMinimizerAt_primary_cone_secondary_graphs line 710
  19. theorem OAI.CubicTorus.MovingCenter.isMinimizerAt_rescaled_normal_equicontinuity line 774