OAI/Geometry/CubicTorus/Regularity/SurfaceH1Tangency.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.normalMeasure_surfaceH1_chart_weak_gradient line 14
  2. lemma OAI.CubicTorus.normalPairing_memLp line 63
  3. def OAI.CubicTorus.surfaceNormalPairing line 73
  4. lemma OAI.CubicTorus.surfaceNormalPairing_ae line 78
  5. lemma OAI.CubicTorus.smoothScalarGradient_tangent line 90
  6. lemma OAI.CubicTorus.surfaceSmoothJet_tangent line 97
  7. theorem OAI.CubicTorus.surfaceH1_tangent line 107
  8. lemma OAI.CubicTorus.graphCovector_metric_pairing line 135
  9. lemma OAI.CubicTorus.smoothScalarGradient_graph_pairing line 150
  10. lemma OAI.CubicTorus.graph_area_integral line 162
  11. def OAI.CubicTorus.periodicGraphScalar line 207
  12. lemma OAI.CubicTorus.periodicGraphScalar_germ line 214
  13. lemma OAI.CubicTorus.periodicGraphScalar_zero_germ line 223
  14. lemma OAI.CubicTorus.periodicGraphScalar_graph_germ line 234
  15. lemma OAI.CubicTorus.periodicGraphScalar_graph_value line 259
  16. lemma OAI.CubicTorus.periodicGraphScalar_graph_covector line 271
  17. lemma OAI.CubicTorus.surfaceJacobiB_smooth_integral line 297
  18. lemma OAI.CubicTorus.periodicGraphScalar_zero_jet line 317
  19. lemma OAI.CubicTorus.surfaceJacobiB_periodicGraphScalar_weight line 331
  20. theorem OAI.CubicTorus.surfaceJacobiB_chart_form line 361
  21. lemma OAI.CubicTorus.L2_measure_scalar_test_integrable line 432
  22. lemma OAI.CubicTorus.L2_measure_vector_test_integrable line 436
  23. theorem OAI.CubicTorus.PlaneWeakGradientOn.vector_ibp line 442
  24. lemma OAI.CubicTorus.planeDivergence_hasCompactSupport line 490
  25. theorem OAI.CubicTorus.PlaneWeakGradientOn.ground_state line 499
  26. lemma OAI.CubicTorus.PlaneWeakGradientOn.toWeakGradient line 584
  27. lemma OAI.CubicTorus.L2_measure_direction_test_integrable line 599
  28. theorem OAI.CubicTorus.PlaneWeakGradientOn.mul_smooth line 610
  29. theorem OAI.CubicTorus.PlaneWeakGradientOn.linearize line 670
  30. theorem OAI.CubicTorus.weak_cmc_graph_jacobi_linearization line 712
  31. lemma OAI.CubicTorus.continuous_indicator_positive_piece line 749
  32. theorem OAI.CubicTorus.IsPositiveNodalPiece.continuous_value line 776
  33. lemma OAI.CubicTorus.nodalSurfaceValue_descent line 797