OAI/Geometry/CubicTorus/Regularity/BVPlanarEssentialBoundary.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.planarSlope_quasiMeasurePreserving line 15
  2. theorem OAI.CubicTorus.moving_product_angular_boundary_subsingleton line 20
  3. theorem OAI.CubicTorus.minimizing_planar_chart_single_transition line 65
  4. def OAI.CubicTorus.planarEssentialBoundary line 109
  5. lemma OAI.CubicTorus.planarEssentialBoundary_compl line 112
  6. lemma OAI.CubicTorus.mem_planarEssentialBoundary_iff line 117
  7. lemma OAI.CubicTorus.measureSupport_local_ae_mono line 123
  8. lemma OAI.CubicTorus.planar_boundary_local_ae line 138
  9. lemma OAI.CubicTorus.measureSupport_preimage_image line 144
  10. lemma OAI.CubicTorus.planar_boundary_preimage_image line 160
  11. lemma OAI.CubicTorus.planar_boundary_isometry line 165
  12. lemma OAI.CubicTorus.continuousAt_planarWedgeCoordinates line 173
  13. lemma OAI.CubicTorus.planar_boundary_angular_transition line 179
  14. lemma OAI.CubicTorus.planar_cone_boundary_contract line 210
  15. theorem OAI.CubicTorus.planar_cone_boundary_chart_unique_slope line 223
  16. lemma OAI.CubicTorus.planar_equal_positive_slopes_collinear line 276
  17. def OAI.CubicTorus.planarNormalRotation line 310
  18. lemma OAI.CubicTorus.planarNormalRotation_axis line 313
  19. lemma OAI.CubicTorus.planarNormalRotation_radial line 318
  20. lemma OAI.CubicTorus.planar_common_hemisphere_or_collinear line 327
  21. theorem OAI.CubicTorus.planar_cone_boundary_collinear line 368
  22. theorem OAI.CubicTorus.connected_planar_phase line 407
  23. lemma OAI.CubicTorus.planar_punctured_ball_preconnected line 440
  24. theorem OAI.CubicTorus.planar_boundary_nonzero line 470
  25. lemma OAI.CubicTorus.planar_hyperplane_volume_zero line 505
  26. lemma OAI.CubicTorus.planar_halfballs_null line 513
  27. lemma OAI.CubicTorus.planar_opposite_halfballs_model line 526
  28. theorem OAI.CubicTorus.planar_boundary_line_halfplane line 545
  29. lemma OAI.CubicTorus.exists_planar_perpendicular line 580
  30. theorem OAI.CubicTorus.planar_cone_halfplane_of_single_transition line 596
  31. lemma OAI.CubicTorus.exists_volumeSupport_in_ball line 628
  32. lemma OAI.CubicTorus.isMinimizerAt_positive_ball_density line 637
  33. lemma OAI.CubicTorus.integral_indicator_ball_real line 660
  34. theorem OAI.CubicTorus.isMinimizerAt_moving_limit_density line 667
  35. lemma OAI.CubicTorus.volume_real_translate_ball line 731
  36. theorem OAI.CubicTorus.isMinimizerAt_primary_limit_density line 752
  37. lemma OAI.CubicTorus.cover_indicator_compl line 814
  38. lemma OAI.CubicTorus.blowupCharacteristic_compl line 819
  39. lemma OAI.CubicTorus.complement_blowup_error line 824
  40. lemma OAI.CubicTorus.complement_cover_error line 831
  41. theorem OAI.CubicTorus.secondary_limit_volume_density line 838
  42. theorem OAI.CubicTorus.isMinimizerAt_secondary_two_sided_density line 873