OAI/Geometry/CubicTorus/Regularity/TorusC1Boundary.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.strict_C1_cone_halfspace line 13
  2. lemma OAI.CubicTorus.quadratic_normal_closedBall_mass line 60
  3. theorem OAI.CubicTorus.isMinimizerAt_primary_halfspace line 83
  4. theorem OAI.CubicTorus.isMinimizerAt_centered_C1_graph line 139
  5. lemma OAI.CubicTorus.volumeSupport_translation line 237
  6. lemma OAI.CubicTorus.openRepresentative_translation line 252
  7. lemma OAI.CubicTorus.frontier_openRepresentative_translation line 259
  8. def OAI.CubicTorus.TorusC1BoundaryAt line 277
  9. theorem OAI.CubicTorus.isMinimizerAt_C1_boundary line 286
  10. lemma OAI.CubicTorus.torusVolume_lift_ball line 327
  11. lemma OAI.CubicTorus.coverEssentialBoundary_lift_iff line 341
  12. lemma OAI.CubicTorus.isMinimizerAt_lifted_boundary line 377
  13. theorem OAI.CubicTorus.isMinimizerAt_centered_phase_patch line 397
  14. theorem OAI.CubicTorus.normalMeasure_C1graph_CMC line 465
  15. lemma OAI.CubicTorus.reverseNormal_local_CMC line 506
  16. theorem OAI.CubicTorus.isMinimizerAt_centered_CMC_graph line 535
  17. theorem OAI.CubicTorus.CMC_graph_weak_equation line 603
  18. def OAI.CubicTorus.cmcFlux line 688
  19. def OAI.CubicTorus.WeakCMCGraph line 690
  20. theorem OAI.CubicTorus.isMinimizerAt_centered_weakCMC_graph line 694
  21. def OAI.CubicTorus.cmcWeight line 756
  22. def OAI.CubicTorus.cmcJacobian line 758
  23. lemma OAI.CubicTorus.cmcWeight_pos line 762
  24. lemma OAI.CubicTorus.cmcWeight_sq line 764
  25. lemma OAI.CubicTorus.cmcWeight_ge_one line 766
  26. lemma OAI.CubicTorus.cmcWeight_le_two line 770
  27. lemma OAI.CubicTorus.cmcWeight_contDiff line 774
  28. lemma OAI.CubicTorus.cmcFlux_contDiff line 779
  29. lemma OAI.CubicTorus.cmcWeight_hasFDerivAt line 782
  30. lemma OAI.CubicTorus.cmcFlux_hasFDerivAt line 796
  31. lemma OAI.CubicTorus.cmcJacobian_apply line 810
  32. lemma OAI.CubicTorus.cmcJacobian_self line 816
  33. lemma OAI.CubicTorus.cmcJacobian_coercive line 823
  34. lemma OAI.CubicTorus.cmcJacobian_norm_le line 836