OAI/Geometry/CubicTorus/Curvature/CMCFrameOperator.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.plane_interior_ball_at_frontier line 13
  2. lemma OAI.CubicTorus.planeElliptic_continue_ball line 58
  3. theorem OAI.CubicTorus.planeElliptic_unique_continuation line 78
  4. def OAI.CubicTorus.planeSymbolDrift line 122
  5. lemma OAI.CubicTorus.planeDivergence_symbol line 126
  6. lemma OAI.CubicTorus.cmc_compress_hessian_trace line 149
  7. lemma OAI.CubicTorus.cmc_frame_operator line 164
  8. lemma OAI.CubicTorus.cmc_frame_ellipticity line 177
  9. lemma OAI.CubicTorus.cmc_frame_bound line 188
  10. lemma OAI.CubicTorus.planeSymbolDrift_continuous line 208
  11. theorem OAI.CubicTorus.LinearCMCEquation.hopf line 215
  12. lemma OAI.CubicTorus.cmcJacobian_strict_coercive line 260
  13. theorem OAI.CubicTorus.LinearCMCEquation.unique_continuation line 270
  14. theorem OAI.CubicTorus.actual_centered_normal_linear_chart line 292
  15. theorem OAI.CubicTorus.isMinimizerAt_normal_linear_chart line 433
  16. lemma OAI.CubicTorus.LinearCMCEquation.affine_zero line 506
  17. def OAI.CubicTorus.normalTranslationNumerator line 537
  18. lemma OAI.CubicTorus.normalTranslationNumerator_contDiff line 540
  19. lemma OAI.CubicTorus.normalTranslationNumerator_eq line 545
  20. lemma OAI.CubicTorus.normalTranslationNumerator_linear line 553
  21. lemma OAI.CubicTorus.normalTranslationNumerator_weight line 568
  22. lemma OAI.CubicTorus.contDiffAt_occupied_graph_transition line 592
  23. theorem OAI.CubicTorus.isMinimizerAt_H1_jacobi_parametric_smooth line 623
  24. lemma OAI.CubicTorus.quotient_graph_closure line 656
  25. lemma OAI.CubicTorus.planar_positive_piece_frontier_zero line 684
  26. def OAI.CubicTorus.relativeZeroNeighborhood line 708
  27. lemma OAI.CubicTorus.relativeZeroNeighborhood_zero line 711
  28. lemma OAI.CubicTorus.quotient_graph_zero_germ line 716
  29. lemma OAI.CubicTorus.preconnected_zero_of_closed_germ line 742
  30. theorem OAI.CubicTorus.isMinimizerAt_normal_zero_germs_closed line 772
  31. theorem OAI.CubicTorus.isMinimizerAt_normal_unique_continuation line 838