OAI/Geometry/CubicTorus/Regularity/BVMovingOrientedReplacement.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CubicTorus.MovingCenter.torusGraphRegion_symmDiff_real_ball_le line 16
2. theorem OAI.CubicTorus.MovingCenter.exists_physical_smooth_graph line 29
3. theorem OAI.CubicTorus.MovingCenter.isMinimizerAt_smooth_trapped_approximation line 79
4. theorem OAI.CubicTorus.MovingCenter.weakCMC_spatial_normalized_residual line 161
5. theorem OAI.CubicTorus.MovingCenter.weakCMC_normalized_sequence_harmonic line 210
6. theorem OAI.CubicTorus.MovingCenter.isMinimizerAt_trapped_harmonic_graphs line 262
7. lemma OAI.CubicTorus.MovingCenter.radialDensityWeight_cell_support line 353
8. lemma OAI.CubicTorus.MovingCenter.radialDensityWeight_periodize line 364
9. def OAI.CubicTorus.MovingCenter.bundleOrientedExcess line 399
10. lemma OAI.CubicTorus.MovingCenter.bundleOrientedExcess_eq line 402
11. theorem OAI.CubicTorus.MovingCenter.isMinimizerAt_oriented_graph_replacement line 410
12. lemma OAI.CubicTorus.MovingCenter.bundleOrientedExcess_nonneg line 484
13. lemma OAI.CubicTorus.MovingCenter.bundleOrientedExcess_mono line 491
14. theorem OAI.CubicTorus.MovingCenter.isMinimizerAt_oriented_interior_low_slice line 517
15. lemma OAI.CubicTorus.MovingCenter.torusGraphRegion_interior_symmDiff line 590
16. lemma OAI.CubicTorus.MovingCenter.radial_sublevelVolume_le line 625
17. theorem OAI.CubicTorus.MovingCenter.isMinimizerAt_scaled_graph_comparison line 645
18. theorem OAI.CubicTorus.MovingCenter.isMinimizerAt_sequential_oriented_decay line 726