OAI/Geometry/CubicTorus/Estimates/BVSecondaryPlanarData.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.actual_secondary_planar_cone_data line 15
  2. lemma OAI.CubicTorus.planar_product_ball_volume_le line 88
  3. theorem OAI.CubicTorus.planar_product_two_sided_density line 131
  4. theorem OAI.CubicTorus.minimizing_planar_product_halfplane line 169
  5. lemma OAI.CubicTorus.normalColumnChart_transverse_inner line 221
  6. theorem OAI.CubicTorus.planar_halfspace_lift line 228
  7. lemma OAI.CubicTorus.blowup_normal_closedBall_mass line 284
  8. theorem OAI.CubicTorus.isMinimizerAt_blowup_perimeter_eq line 299
  9. theorem OAI.CubicTorus.isMinimizerAt_blowup_local_minimal line 341
  10. lemma OAI.CubicTorus.blowupNormal_inner_integrable line 385
  11. lemma OAI.CubicTorus.radial_normal_flux_tendsto line 393
  12. lemma OAI.CubicTorus.flat_set_limit_flux_on_ball line 426
  13. lemma OAI.CubicTorus.flat_set_limit_density line 455
  14. theorem OAI.CubicTorus.flat_set_limit_normal line 472
  15. theorem OAI.CubicTorus.conical_halfspace_extend line 522
  16. lemma OAI.CubicTorus.coverLocalPerimeter_halfspace_ball line 552
  17. lemma OAI.CubicTorus.halfspace_model_perimeter_ball line 567
  18. theorem OAI.CubicTorus.actual_secondary_halfspace line 593
  19. theorem OAI.CubicTorus.isMinimizerAt_minimizing_cone_blowup line 687
  20. theorem OAI.CubicTorus.isMinimizerAt_primary_cone_flat_secondary line 758
  21. theorem OAI.CubicTorus.actual_tangent_secondary_centered_representation line 809