OAI/Geometry/CubicTorus/Regularity/SurfaceNormalReverse.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.restricted_L2_extension line 13
  2. theorem OAI.CubicTorus.PlaneWeakGradientOn.cmc_classical_near line 23
  3. theorem OAI.CubicTorus.PlaneWeakGradientOn.cmc_smoothAt line 92
  4. lemma OAI.CubicTorus.continuous_memLp_top_ball line 126
  5. theorem OAI.CubicTorus.PlaneWeakGradientOn.weighted_L2 line 133
  6. theorem OAI.CubicTorus.PlaneWeakGradientOn.jacobi_smoothAt line 154
  7. theorem OAI.CubicTorus.surfaceH1_jacobi_graph_smoothAt line 215
  8. lemma OAI.CubicTorus.reverseNormal_reverseNormal line 296
  9. lemma OAI.CubicTorus.reverseNormal_measurePreserving line 302
  10. lemma OAI.CubicTorus.reverseNormal_measurePreserving_back line 306
  11. def OAI.CubicTorus.normalReverseLp line 314
  12. lemma OAI.CubicTorus.normalReverseLp_ae line 320
  13. lemma OAI.CubicTorus.smoothScalarValue_reverse line 326
  14. lemma OAI.CubicTorus.smoothScalarGradient_reverse line 329
  15. def OAI.CubicTorus.surfaceJetReverse line 335
  16. lemma OAI.CubicTorus.surfaceJetReverse_smooth line 340
  17. theorem OAI.CubicTorus.surfaceH1_reverse line 364
  18. lemma OAI.CubicTorus.surfaceMultiplier_reverse line 370
  19. lemma OAI.CubicTorus.surfaceJacobiB_reverse line 386
  20. lemma OAI.CubicTorus.surfaceJacobi_homogeneous_of_smooth line 398
  21. theorem OAI.CubicTorus.surfaceJacobi_homogeneous_reverse line 409
  22. lemma OAI.CubicTorus.smooth_graph_extension_compact line 437
  23. lemma OAI.CubicTorus.smooth_graph_symbol_extension line 455
  24. theorem OAI.CubicTorus.WeakCMCGraph.smooth_jacobi_data line 496
  25. theorem OAI.CubicTorus.surfaceCurvatureLp_graph_ae line 548
  26. lemma OAI.CubicTorus.surfaceCurvatureLp_reverse line 590
  27. theorem OAI.CubicTorus.normalMeasure_H1_jacobi_graph_smoothAt line 615
  28. theorem OAI.CubicTorus.normalMeasure_H1_jacobi_signed_graph_smoothAt line 690
  29. theorem OAI.CubicTorus.isMinimizerAt_centered_H1_jacobi_smooth line 763