OAI/Geometry/CubicTorus/Profiles/CenteredJacobiChart.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.CubicTorus.CenteredJacobiChart line 13
  2. theorem OAI.CubicTorus.isMinimizerAt_centeredJacobiChart line 54
  3. lemma OAI.CubicTorus.integral_normal_cover_position line 138
  4. theorem OAI.CubicTorus.normalMeasure_graph_integral line 149
  5. lemma OAI.CubicTorus.graphSlopeNormal_inner_graphDerivative line 206
  6. lemma OAI.CubicTorus.normalGraph_translated_tangency line 225
  7. lemma OAI.CubicTorus.normalGraph_trace_gradient line 248
  8. theorem OAI.CubicTorus.graphTangentialGradient_trace line 271
  9. theorem OAI.CubicTorus.graph_compact_test_extension line 296
  10. theorem OAI.CubicTorus.compact_test_periodization line 339
  11. lemma OAI.CubicTorus.sibling_surfaceJacobiB_cutoff_commutator line 360
  12. theorem OAI.CubicTorus.surfaceH1_weak_wronskian line 395
  13. lemma OAI.CubicTorus.normalProjection_measurePreserving line 419
  14. def OAI.CubicTorus.spatialPullback line 424
  15. lemma OAI.CubicTorus.spatialPullback_continuousMap line 430
  16. lemma OAI.CubicTorus.surfaceSmoothJet_value_spatial line 445
  17. lemma OAI.CubicTorus.surfaceSmoothJet_gradient_spatial line 456
  18. theorem OAI.CubicTorus.surfaceH1_spatial_descent line 485
  19. def OAI.CubicTorus.dominatedL2Pullback line 518
  20. lemma OAI.CubicTorus.dominatedL2Pullback_ae line 526
  21. def OAI.CubicTorus.spatialPushdown line 537
  22. lemma OAI.CubicTorus.spatialPushdown_pullback line 543
  23. lemma OAI.CubicTorus.spatialPullback_pushdown line 549
  24. def OAI.CubicTorus.surfaceChartPullback line 556
  25. lemma OAI.CubicTorus.surfaceChartPullback_continuousMap line 565
  26. lemma OAI.CubicTorus.surfaceH1_spatial_representatives line 596
  27. def OAI.CubicTorus.normalProjectedGradient line 615
  28. lemma OAI.CubicTorus.continuous_normalProjectedGradient line 618
  29. theorem OAI.CubicTorus.localized_wronskian_graph_integral line 624
  30. lemma OAI.CubicTorus.normalProjectedGradient_sign line 694
  31. lemma OAI.CubicTorus.normalProjectedGradient_graph_trace line 701
  32. lemma OAI.CubicTorus.plane_gradient_const_div line 710
  33. theorem OAI.CubicTorus.graph_wronskian_ground_state line 717
  34. lemma OAI.CubicTorus.graphHeightExtension_eventually_zero line 759
  35. lemma OAI.CubicTorus.gradient_eq_zero_of_graph_extension_germ line 771
  36. lemma OAI.CubicTorus.graphSlopeNormal_inner_axis line 778