OAI/Geometry/CubicTorus/Estimates/GraphInverseMetric.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.isMinimizerAt_normal_patch line 13
  2. theorem OAI.CubicTorus.isMinimizerAt_global_normal line 69
  3. theorem OAI.CubicTorus.Periodic.isMinimizerAt_global_normal_stability line 100
  4. theorem OAI.CubicTorus.continuous_periodic_descent line 131
  5. theorem OAI.CubicTorus.isMinimizerAt_periodic_ae_eq_boundary line 147
  6. theorem OAI.CubicTorus.actual_centered_normal_graph_chart line 183
  7. theorem OAI.CubicTorus.Periodic.isMinimizerAt_boundary_normal_stability line 334
  8. lemma OAI.CubicTorus.regularizedNormal_eventuallyEq line 375
  9. theorem OAI.CubicTorus.Periodic.isMinimizerAt_tubular_normal_stability line 382
  10. theorem OAI.CubicTorus.isMinimizerAt_normal_graph_chart line 434
  11. lemma OAI.CubicTorus.LinearCMCEquation.classical_zero line 503
  12. theorem OAI.CubicTorus.plane_weight_harmonic_potential line 513
  13. def OAI.CubicTorus.graphInverseMetric line 572
  14. lemma OAI.CubicTorus.graphInverseMetric_identity line 575
  15. def OAI.CubicTorus.graphTangentialGradient line 583
  16. lemma OAI.CubicTorus.graphTangentialGradient_duality line 586
  17. lemma OAI.CubicTorus.graphTangentialGradient_inner line 593
  18. lemma OAI.CubicTorus.cmc_graph_curvature_potential line 601
  19. theorem OAI.CubicTorus.cmcGraphJacobi_geometric line 617
  20. lemma OAI.CubicTorus.graphInverseMetric_slope line 650
  21. lemma OAI.CubicTorus.graph_metric_projection line 662
  22. lemma OAI.CubicTorus.normal_trace_square_invariance line 699
  23. theorem OAI.CubicTorus.graph_normal_extension_curvature line 732
  24. lemma OAI.CubicTorus.normal_trace_invariance line 805