OAI/Geometry/CubicTorus/Estimates/BVLocalScaling.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CubicTorus.line_invariant_local_product line 15
2. def OAI.CubicTorus.affineCoverRegion line 90
3. lemma OAI.CubicTorus.measurableSet_affineCoverRegion line 93
4. lemma OAI.CubicTorus.divergence_affine_pullback line 96
5. lemma OAI.CubicTorus.tsupport_affine_pullback line 105
6. lemma OAI.CubicTorus.integral_divergence_affineCoverRegion line 116
7. theorem OAI.CubicTorus.affineCoverRegion_flux_le line 136
8. def OAI.CubicTorus.torusCoverRegion line 163
9. lemma OAI.CubicTorus.measurableSet_torusCoverRegion line 165
10. lemma OAI.CubicTorus.characteristic_torusCoverRegion line 168
11. lemma OAI.CubicTorus.interior_cutoff_flux_eq_set line 175
12. lemma OAI.CubicTorus.torus_affine_radial_flux_le line 201
13. lemma OAI.CubicTorus.torus_affine_symmDiff_support line 235
14. lemma OAI.CubicTorus.torus_affine_symmDiff_volume line 252
15. theorem OAI.CubicTorus.isMinimizerAt_local_flux_replacement line 298
16. theorem OAI.CubicTorus.isMinimizerAt_local_flux_low_slice line 325
17. lemma OAI.CubicTorus.MovingCenter.torus_affine_radial_flux_le line 395
18. lemma OAI.CubicTorus.MovingCenter.torus_affine_symmDiff_support line 417
19. lemma OAI.CubicTorus.MovingCenter.torus_affine_symmDiff_volume line 434
20. lemma OAI.CubicTorus.MovingCenter.normalMeasure_radial_sublevel line 480
21. theorem OAI.CubicTorus.MovingCenter.isMinimizerAt_local_flux_low_slice line 493
22. theorem OAI.CubicTorus.MovingCenter.isMinimizerAt_scaled_set_replacement line 562
23. lemma OAI.CubicTorus.moving_blowup_flux_tendsto line 620
24. lemma OAI.CubicTorus.blowup_flux_le_scaled_mass line 650
25. theorem OAI.CubicTorus.isMinimizerAt_scaled_set_replacement line 700
26. lemma OAI.CubicTorus.density_scaled_mass_tendsto line 758
27. lemma OAI.CubicTorus.blowup_error_integrable line 772
28. theorem OAI.CubicTorus.isMinimizerAt_blowup_competitor_bound line 785