OAI/Geometry/CubicTorus/Estimates/BVAnnulusSelection.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.torusGraphRegion_interior_symmDiff line 15
  2. lemma OAI.CubicTorus.radial_sublevelVolume_le line 62
  3. lemma OAI.CubicTorus.plane_relative_gradient_norm line 69
  4. theorem OAI.CubicTorus.isMinimizerAt_graph_interpolation_comparison line 73
  5. def OAI.CubicTorus.planeAnnulus line 128
  6. lemma OAI.CubicTorus.planeAnnulus_pairwise line 131
  7. lemma OAI.CubicTorus.planeAnnulus_subset line 143
  8. lemma OAI.CubicTorus.planeAnnulus_integral_pigeonhole line 150
  9. lemma OAI.CubicTorus.finite_subsequence_constant line 172
  10. lemma OAI.CubicTorus.plane_fderiv_relative_integrable line 193
  11. lemma OAI.CubicTorus.exists_plane_interpolation_bump line 199
  12. theorem OAI.CubicTorus.strong_L2_annulus_replacement line 212
  13. lemma OAI.CubicTorus.lipschitz_mul_of_bound_on_support line 300
  14. lemma OAI.CubicTorus.exists_lipschitz_cutoff_mul line 329
  15. theorem OAI.CubicTorus.local_planar_H1_harmonic_approximation line 357
  16. lemma OAI.CubicTorus.lipschitz_centered_scale line 438
  17. lemma OAI.CubicTorus.lipschitz_centered_scale_gradient line 450
  18. lemma OAI.CubicTorus.lipschitz_centered_scale_gradient_integral line 460
  19. theorem OAI.CubicTorus.planar_normalized_H1 line 469
  20. lemma OAI.CubicTorus.centered_scale_laplacian_pairing line 495
  21. def OAI.CubicTorus.normalColumnCutoff line 521
  22. lemma OAI.CubicTorus.normalColumnCutoff_tsupport line 527
  23. lemma OAI.CubicTorus.normalColumnCutoff_eventually_one line 534
  24. lemma OAI.CubicTorus.normalColumnCutoff_one line 541
  25. lemma OAI.CubicTorus.normalColumnCutoff_deriv_zero line 545
  26. lemma OAI.CubicTorus.normalColumnCutoff_second_zero line 550
  27. lemma OAI.CubicTorus.normalColumnTest_tsupport_ball line 555
  28. lemma OAI.CubicTorus.trapped_column_characteristic line 573
  29. lemma OAI.CubicTorus.integral_column_negative_indicator line 621
  30. lemma OAI.CubicTorus.integrableOn_column_bounded line 634
  31. lemma OAI.CubicTorus.integral_column_cutoff line 638
  32. lemma OAI.CubicTorus.integral_column_cutoff_second line 687
  33. lemma OAI.CubicTorus.columnCutoff_second_contDiff line 729
  34. lemma OAI.CubicTorus.columnCutoff_second_hasCompactSupport line 734
  35. theorem OAI.CubicTorus.integral_column_laplacian line 739
  36. theorem OAI.CubicTorus.weakCMC_column_height_identity line 819