OAI/Geometry/CubicTorus/Reflection/SiblingReflectNormal.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.normalized_CMC_common_patch_curvature line 13
  2. theorem OAI.CubicTorus.CMC_surfaces_identity line 42
  3. lemma OAI.CubicTorus.boundaryZeroGerm_homeomorph line 77
  4. lemma OAI.CubicTorus.boundaryZeroGerm_translation line 85
  5. theorem OAI.CubicTorus.isMinimizerAt_Jacobi_zero_germ_closed line 93
  6. theorem OAI.CubicTorus.isMinimizerAt_Jacobi_identity line 145
  7. theorem OAI.CubicTorus.CenteredJacobiChart.zero_germ_of_local_nonneg line 176
  8. theorem OAI.CubicTorus.isMinimizerAt_Jacobi_strong_minimum line 219
  9. theorem OAI.CubicTorus.isMinimizerAt_center_normal_unique line 290
  10. theorem OAI.CubicTorus.isMinimizerAt_normal_unique line 389
  11. def OAI.CubicTorus.sibling_reflectNormal line 440
  12. lemma OAI.CubicTorus.sibling_measurable_reflectNormal line 444
  13. lemma OAI.CubicTorus.sibling_reflectNormal_periodic_eval line 451
  14. theorem OAI.CubicTorus.isNormalMeasure_firstReflection line 457
  15. lemma OAI.CubicTorus.graph_tangent_of_graph_containment line 493
  16. lemma OAI.CubicTorus.graphSlopeNormal_gradient_zero line 516
  17. theorem OAI.CubicTorus.normalized_CMC_common_germ_normals line 521
  18. theorem OAI.CubicTorus.normalized_CMC_common_germ_oriented line 555
  19. theorem OAI.CubicTorus.HasNormalizedCMCCharts.neg line 592
  20. theorem OAI.CubicTorus.CMC_surfaces_unoriented_identity line 627
  21. theorem OAI.CubicTorus.CMC_surface_oriented_subset line 666
  22. theorem OAI.CubicTorus.CMC_surface_unoriented_subset line 680
  23. theorem OAI.CubicTorus.isMinimizerAt_lifted_boundary_global line 716
  24. lemma OAI.CubicTorus.lifted_ae_eq_torus line 737
  25. def OAI.CubicTorus.coverAEAgreement line 760
  26. lemma OAI.CubicTorus.isOpen_coverAEAgreement line 763
  27. lemma OAI.CubicTorus.mem_coverAEAgreement_iff line 766
  28. lemma OAI.CubicTorus.coverAEAgreement_trans line 789
  29. lemma OAI.CubicTorus.coverAEAgreement_symm line 799
  30. lemma OAI.CubicTorus.coverAEAgreement_compl line 804
  31. lemma OAI.CubicTorus.coverAEAgreement_disjoint line 809
  32. lemma OAI.CubicTorus.ae_eq_of_coverAEAgreement_univ line 820
  33. theorem OAI.CubicTorus.cover_local_phase_global line 830