OAI/Geometry/CubicTorus/Profiles/NormalizedCMCCharts.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.sibling_normalGraph_regraph_normal line 13
  2. theorem OAI.CubicTorus.isMinimizerAt_normalized_CMC_chart line 82
  3. lemma OAI.CubicTorus.normalGraph_injective line 144
  4. lemma OAI.CubicTorus.normalGraph_height_eq line 150
  5. theorem OAI.CubicTorus.normal_graph_germ_coincidence line 157
  6. lemma OAI.CubicTorus.isOpenMap_quotientMap line 218
  7. lemma OAI.CubicTorus.isOpenMap_shiftedQuotient line 225
  8. lemma OAI.CubicTorus.shiftedQuotient_nhds line 228
  9. def OAI.CubicTorus.HasNormalizedCMCCharts line 233
  10. lemma OAI.CubicTorus.isMinimizerAt_hasNormalizedCMCCharts line 242
  11. def OAI.CubicTorus.orientedSurfaceAgreement line 255
  12. lemma OAI.CubicTorus.isOpen_orientedSurfaceAgreement line 258
  13. theorem OAI.CubicTorus.cmc_strong_minimum line 273
  14. def OAI.CubicTorus.boundaryZeroGerm line 322
  15. lemma OAI.CubicTorus.boundaryZeroGerm_open line 325
  16. lemma OAI.CubicTorus.CenteredJacobiChart.zero_trace_germ line 328
  17. theorem OAI.CubicTorus.CenteredJacobiChart.zero_germ_closed line 347
  18. def OAI.CubicTorus.sibling_smoothScalarTranslate line 406
  19. lemma OAI.CubicTorus.smoothScalarTranslate_gradient line 412
  20. lemma OAI.CubicTorus.sibling_translateNormal_measurePreserving line 420
  21. def OAI.CubicTorus.normalTranslatePullback line 425
  22. def OAI.CubicTorus.normalTranslateJet line 431
  23. lemma OAI.CubicTorus.normalTranslateJet_ae line 436
  24. lemma OAI.CubicTorus.normalTranslateJet_smooth line 444
  25. lemma OAI.CubicTorus.normalTranslateJet_mem_surfaceH1 line 483
  26. lemma OAI.CubicTorus.normalTranslate_multiplier line 507
  27. lemma OAI.CubicTorus.normalTranslate_Jacobi line 530
  28. lemma OAI.CubicTorus.normalTranslate_one line 545
  29. lemma OAI.CubicTorus.normalTranslate_mean line 550
  30. def OAI.CubicTorus.normalTranslateField line 559
  31. lemma OAI.CubicTorus.normalTranslateField_smooth line 561
  32. lemma OAI.CubicTorus.normalTranslateField_periodic line 565
  33. lemma OAI.CubicTorus.normalTranslateField_fderiv line 572
  34. lemma OAI.CubicTorus.normalTranslate_curvature line 580
  35. lemma OAI.CubicTorus.normalTranslate_smooth_inverse line 606
  36. lemma OAI.CubicTorus.normalTranslate_directional line 612
  37. lemma OAI.CubicTorus.normalTranslateJet_isometry line 634
  38. lemma OAI.CubicTorus.normalTranslateJet_surjective_H1 line 642
  39. lemma OAI.CubicTorus.sibling_normalProjection_translate line 656
  40. lemma OAI.CubicTorus.normalTranslateField_ae line 661
  41. lemma OAI.CubicTorus.normalTranslateJet_scalar_representative line 676
  42. lemma OAI.CubicTorus.smoothScalarTranslate_descent line 702
  43. lemma OAI.CubicTorus.positiveNodalPiece_translation line 709
  44. lemma OAI.CubicTorus.normalTranslate_weakJacobi line 722
  45. lemma OAI.CubicTorus.normalTranslate_smooth_weakJacobi line 733
  46. theorem OAI.CubicTorus.orientedSurfaceAgreement_closed_at line 756
  47. lemma OAI.CubicTorus.preconnected_subset_of_relative_germ_closed line 823
  48. lemma OAI.CubicTorus.orientedSurfaceAgreement_symm line 839