OAI/Geometry/CubicTorus/Regularity/NormalRotationWeak.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.normalTangentRotation_test_divergence line 13
  2. theorem OAI.CubicTorus.isMinimizerAt_normalTangentRotation_weak_identity line 52
  3. theorem OAI.CubicTorus.isMinimizerAt_exists_rotation_conservation line 97
  4. theorem OAI.CubicTorus.surfaceSmoothJacobi_commutator line 127
  5. lemma OAI.CubicTorus.smoothScalarGradient_of_coordinate_germ line 154
  6. lemma OAI.CubicTorus.smoothScalarGradient_inner_tangent line 169
  7. lemma OAI.CubicTorus.rotation_commutator_density line 193
  8. lemma OAI.CubicTorus.surfaceJacobiB_sub_left line 247
  9. lemma OAI.CubicTorus.smoothJacobi_commutator_integrable line 253
  10. theorem OAI.CubicTorus.isMinimizerAt_rotation_jacobi_from_germs line 267
  11. lemma OAI.CubicTorus.periodicRotationNormalScalar_eq line 338
  12. theorem OAI.CubicTorus.TrueRadialTube.exists_rotation_jacobi line 356
  13. theorem OAI.CubicTorus.PlaneWeakGradientOn.jacobi_equationNear line 410
  14. theorem OAI.CubicTorus.surfaceH1_jacobi_graph_equationNear line 474
  15. theorem OAI.CubicTorus.normalMeasure_H1_jacobi_graph_equationNear line 556
  16. theorem OAI.CubicTorus.normalMeasure_H1_jacobi_signed_graph_equationNear line 632
  17. theorem OAI.CubicTorus.isMinimizerAt_centered_H1_jacobi_equation line 706