OAI/Geometry/CubicTorus/Curvature/MinimizerJacobiEquation.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.isMinimizerAt_H1_jacobi_equation line 13
  2. theorem OAI.CubicTorus.isMinimizerAt_H1_jacobi_zero_germs_closed line 102
  3. theorem OAI.CubicTorus.isMinimizerAt_H1_jacobi_unique_continuation line 184
  4. theorem OAI.CubicTorus.isMinimizerAt_mean_zero_negative_point line 217
  5. theorem OAI.CubicTorus.isMinimizerAt_general_positive_nodal_not_disjoint line 246
  6. lemma OAI.CubicTorus.TrueRadialTube.frontier_preconnected line 327
  7. theorem OAI.CubicTorus.TrueRadialTube.exists_rotation_nodal_restriction line 335
  8. theorem OAI.CubicTorus.TrueRadialTube.exists_rotation_nodal_restriction_null line 358
  9. theorem OAI.CubicTorus.first_transition_nonstandard_rotation_nodal line 397
  10. lemma OAI.CubicTorus.antitoneOn_deriv_nonpos_interior line 434
  11. theorem OAI.CubicTorus.antitone_ac_area_measure line 439
  12. theorem OAI.CubicTorus.antitone_ac_area_substitution line 467
  13. theorem OAI.CubicTorus.isMinimizerAt_axial_area_substitution line 494
  14. lemma OAI.CubicTorus.closed_set_complete_line line 530
  15. lemma OAI.CubicTorus.open_phase_line_invariant line 551
  16. theorem OAI.CubicTorus.isMinimizerAt_zero_normal_flow line 569
  17. theorem OAI.CubicTorus.isMinimizerAt_H1_jacobi_unique_continuation_null line 621
  18. theorem OAI.CubicTorus.isMinimizerAt_normal_unique_continuation_null line 651
  19. theorem OAI.CubicTorus.normalGraph_regraph_transverse line 684
  20. theorem OAI.CubicTorus.isMinimizerAt_transverse_graph_cover line 764