OAI/Geometry/CubicTorus/Profiles/CMCSecantSymbol.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.isMinimizerAt_no_constant_normal_patch line 13
  2. def OAI.CubicTorus.cmcSecant line 110
  3. lemma OAI.CubicTorus.cmcSecant_apply line 116
  4. lemma OAI.CubicTorus.cmcSecant_exact line 122
  5. lemma OAI.CubicTorus.cmcSecant_symmetric line 137
  6. lemma OAI.CubicTorus.cmcWeight_gt_norm line 142
  7. lemma OAI.CubicTorus.cmcSecant_elliptic line 147
  8. lemma OAI.CubicTorus.cmcSecant_contDiff line 171
  9. lemma OAI.CubicTorus.plane_gradient_sub line 196
  10. lemma OAI.CubicTorus.cmcSecant_comp_contDiff line 204
  11. lemma OAI.CubicTorus.cmcSecant_graph_contDiff line 220
  12. lemma OAI.CubicTorus.cmcSecant_graph_flux line 224
  13. lemma OAI.CubicTorus.cmcSecant_graph_divergence line 231
  14. theorem OAI.CubicTorus.cmcGraph_unique_continuation line 240
  15. lemma OAI.CubicTorus.plane_smooth_local_inverse line 272
  16. lemma OAI.CubicTorus.normalPlane_decomposition line 316
  17. lemma OAI.CubicTorus.normalGraph_derivative_tangent line 325
  18. theorem OAI.CubicTorus.normalGraph_regraph line 337
  19. lemma OAI.CubicTorus.unit_normal_graph_unique line 402
  20. lemma OAI.CubicTorus.normalGraph_zero line 436
  21. lemma OAI.CubicTorus.normalGraph_tendsto_zero line 441
  22. theorem OAI.CubicTorus.normalGraph_regraph_normal line 448
  23. lemma OAI.CubicTorus.normalGraph_regraph_cover line 495
  24. theorem OAI.CubicTorus.isMinimizerAt_tangent_CMC_chart line 533
  25. def OAI.CubicTorus.relativeContainmentNeighborhood line 590
  26. lemma OAI.CubicTorus.relativeContainmentNeighborhood_mem line 592
  27. lemma OAI.CubicTorus.quotient_graph_containment_germ line 596
  28. lemma OAI.CubicTorus.preconnected_subset_of_closed_germ line 619
  29. lemma OAI.CubicTorus.normalGraph_eq_height line 637
  30. lemma OAI.CubicTorus.normalGraph_boundary_height line 641
  31. structure OAI.CubicTorus.OrientedCMCCharts line 664
  32. theorem OAI.CubicTorus.isMinimizerAt_oriented_CMC_charts line 676
  33. theorem OAI.CubicTorus.OrientedCMCCharts.containment_germs_closed line 688
  34. theorem OAI.CubicTorus.OrientedCMCCharts.containment_of_patch line 751
  35. theorem OAI.CubicTorus.OrientedCMCCharts.curvature_eq_of_patch line 779
  36. theorem OAI.CubicTorus.OrientedCMCCharts.eq_of_patch line 814