OAI/Geometry/CubicTorus/Curvature/NormalCurvatureScalar.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.normalComponentScalar_null line 13
  2. lemma OAI.CubicTorus.normalComponentScalar_geometry line 45
  3. theorem OAI.CubicTorus.normalComponentScalar_product_sum line 82
  4. lemma OAI.CubicTorus.normal_curvature_contDiff line 139
  5. def OAI.CubicTorus.normalCurvatureScalar line 144
  6. lemma OAI.CubicTorus.normalComponent_one_pairing line 149
  7. theorem OAI.CubicTorus.normalComponentScalar_global_jacobi line 168
  8. theorem OAI.CubicTorus.Periodic.isMinimizerAt_H1_jacobi_system line 224
  9. theorem OAI.CubicTorus.Periodic.isMinimizerAt_H1_translation_jacobi line 260
  10. def OAI.CubicTorus.positiveTrunc line 299
  11. def OAI.CubicTorus.positiveTruncCoeff line 300
  12. lemma OAI.CubicTorus.smoothTransition_deriv_zero_neg line 302
  13. lemma OAI.CubicTorus.smoothTransition_deriv_zero_gt line 309
  14. lemma OAI.CubicTorus.positiveTruncCoeff_zero line 316
  15. lemma OAI.CubicTorus.positiveTruncCoeff_one line 321
  16. lemma OAI.CubicTorus.positiveTruncCoeff_bounded line 324
  17. lemma OAI.CubicTorus.positiveTrunc_contDiff line 340
  18. lemma OAI.CubicTorus.positiveTrunc_hasDerivAt line 343
  19. lemma OAI.CubicTorus.positiveTrunc_bound line 355
  20. lemma OAI.CubicTorus.positiveTrunc_eventually line 361
  21. lemma OAI.CubicTorus.surfaceL2_bounded_convergence line 389
  22. def OAI.CubicTorus.smoothScalarPositiveTrunc line 436
  23. lemma OAI.CubicTorus.gradient_positiveTrunc line 440
  24. lemma OAI.CubicTorus.smoothScalarGradient_positiveTrunc line 452
  25. def OAI.CubicTorus.positiveSurfaceValue line 462
  26. def OAI.CubicTorus.positiveSurfaceGradient line 464
  27. lemma OAI.CubicTorus.positiveSurfaceValue_memLp line 467
  28. lemma OAI.CubicTorus.positiveSurfaceGradient_memLp line 472
  29. def OAI.CubicTorus.positiveSurfaceJet line 478
  30. lemma OAI.CubicTorus.surfaceL2_continuous_bounded_convergence line 494
  31. lemma OAI.CubicTorus.positiveSurfaceJet_mem_surfaceH1 line 511
  32. lemma OAI.CubicTorus.surfaceJacobiB_positive_restriction line 576
  33. lemma OAI.CubicTorus.surfaceJacobiB_positive_null line 608
  34. theorem OAI.CubicTorus.normalComponentScalar_positive_null line 615
  35. def OAI.CubicTorus.directionalNormalScalar line 643
  36. lemma OAI.CubicTorus.directionalNormalScalar_apply line 647
  37. lemma OAI.CubicTorus.surfaceJacobiB_sum_left line 657
  38. lemma OAI.CubicTorus.directionalNormalScalar_global_jacobi line 666
  39. theorem OAI.CubicTorus.Periodic.isMinimizerAt_translation_positive_nodal line 680
  40. lemma OAI.CubicTorus.locallyConnected_of_quotient_graphs line 720
  41. theorem OAI.CubicTorus.isMinimizerAt_boundary_locallyConnected line 768
  42. def OAI.CubicTorus.nodalEpsilon line 798
  43. def OAI.CubicTorus.separatedPositiveTrunc line 799
  44. lemma OAI.CubicTorus.nodalEpsilon_pos line 801
  45. lemma OAI.CubicTorus.separatedPositiveTrunc_contDiff line 803
  46. lemma OAI.CubicTorus.separatedPositiveTrunc_zero line 806
  47. lemma OAI.CubicTorus.separatedPositiveTrunc_bound line 812
  48. lemma OAI.CubicTorus.separatedPositiveTrunc_tendsto line 822