OAI/Geometry/CubicTorus/Curvature/TorusC2CMCAt.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.isMinimizerAt_centered_C1_modulus line 13
  2. theorem OAI.CubicTorus.actual_centered_graph_phase_patch line 121
  3. theorem OAI.CubicTorus.actual_centered_graph_CMC line 193
  4. theorem OAI.CubicTorus.actual_centered_graph_weakCMC line 267
  5. theorem OAI.CubicTorus.isMinimizerAt_centered_holder_CMC line 335
  6. theorem OAI.CubicTorus.isMinimizerAt_centered_C2_graph line 385
  7. def OAI.CubicTorus.TorusC2CMCAt line 404
  8. theorem OAI.CubicTorus.isMinimizerAt_C2_boundary line 414
  9. theorem OAI.CubicTorus.isMinimizerAt_classical_CMC line 456
  10. theorem OAI.CubicTorus.isMinimizerAt_smooth_CMC line 489
  11. lemma OAI.CubicTorus.plane_gradient_mul line 524
  12. lemma OAI.CubicTorus.plane_gradient_contDiff line 532
  13. def OAI.CubicTorus.graphJacobiForm line 537
  14. theorem OAI.CubicTorus.graphJacobiForm_transform line 541
  15. lemma OAI.CubicTorus.plane_inner_components line 610
  16. lemma OAI.CubicTorus.plane_gradient_component line 614
  17. lemma OAI.CubicTorus.planeDivergence_add line 619
  18. lemma OAI.CubicTorus.planeDivergence_smul line 625
  19. lemma OAI.CubicTorus.plane_gradient_weight line 634
  20. lemma OAI.CubicTorus.plane_gradient_div line 649
  21. lemma OAI.CubicTorus.plane_hessian_direction line 675
  22. lemma OAI.CubicTorus.plane_hessian_symmetric line 684
  23. def OAI.CubicTorus.graphShapeOperator line 691
  24. def OAI.CubicTorus.planeTraceSquare line 694
  25. def OAI.CubicTorus.graphSquaredSecondFundamentalForm line 699
  26. lemma OAI.CubicTorus.plane_shape_trace_identity line 702
  27. lemma OAI.CubicTorus.graphSquaredSecondFundamentalForm_formula line 720
  28. def OAI.CubicTorus.planeTrace line 753
  29. lemma OAI.CubicTorus.plane_decompose_sum line 756
  30. lemma OAI.CubicTorus.plane_cover_clm_component line 760
  31. lemma OAI.CubicTorus.cover_plane_clm_component line 767
  32. lemma OAI.CubicTorus.rectangular_trace line 774
  33. lemma OAI.CubicTorus.planeTrace_square line 786
  34. lemma OAI.CubicTorus.planeTrace_neg line 795
  35. lemma OAI.CubicTorus.cmcJacobian_inner_slope line 810
  36. lemma OAI.CubicTorus.normalGraph_fderiv_apply line 818
  37. lemma OAI.CubicTorus.graphSlopeNormal_weight line 825
  38. theorem OAI.CubicTorus.graph_weingarten line 831