OAI/Geometry/CubicTorus/Profiles/FirstAxisShift.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicTorus.firstAxisShift line 13
  2. def OAI.CubicTorus.firstHalfMass line 15
  3. lemma OAI.CubicTorus.integrable_shifted_characteristic line 19
  4. lemma OAI.CubicTorus.firstHalfMass_lipschitz line 24
  5. lemma OAI.CubicTorus.firstSeam_shift_half line 52
  6. lemma OAI.CubicTorus.firstHalfMass_pair line 64
  7. lemma OAI.CubicTorus.firstHalfMass_eq_volume line 94
  8. theorem OAI.CubicTorus.exists_first_half_bisection line 113
  9. theorem OAI.CubicTorus.exists_bisected_reflection_minimizers line 127
  10. lemma OAI.CubicTorus.firstSeam_sign line 150
  11. lemma OAI.CubicTorus.first_half_image line 169
  12. lemma OAI.CubicTorus.isOpen_first_half line 181
  13. lemma OAI.CubicTorus.isPreconnected_first_half line 185
  14. lemma OAI.CubicTorus.first_half_volume line 192
  15. lemma OAI.CubicTorus.reflected_half_agrees line 200
  16. lemma OAI.CubicTorus.reflectionClosure_invariant line 224
  17. theorem OAI.CubicTorus.isMinimizerAt_eq_bisected_reflection line 230
  18. theorem OAI.CubicTorus.isMinimizerAt_bisected_reflection_invariant line 263
  19. theorem OAI.CubicTorus.isMinimizerAt_exists_first_reflection line 273
  20. lemma OAI.CubicTorus.reflectionPullback_normal_ae line 306
  21. theorem OAI.CubicTorus.isMinimizerAt_reflection_normal line 323
  22. theorem OAI.CubicTorus.isMinimizerAt_reflection_seam_normal line 344
  23. lemma OAI.CubicTorus.firstSeam_zero_fixed line 373
  24. theorem OAI.CubicTorus.isMinimizerAt_reflection_boundary line 392
  25. lemma OAI.CubicTorus.isMinimizerAt_reflection_normal_scalar line 416
  26. lemma OAI.CubicTorus.isMinimizerAt_firstSeam_normal_zero line 436
  27. lemma OAI.CubicTorus.positive_derivative_negative_on_left line 461
  28. lemma OAI.CubicTorus.differentiable_piece_contradiction line 473
  29. lemma OAI.CubicTorus.line_to_ball_inside line 511
  30. theorem OAI.CubicTorus.cmc_nodal_piece_C1_impossible line 519
  31. theorem OAI.CubicTorus.CenteredJacobiChart.nodal_truncation_impossible line 576
  32. theorem OAI.CubicTorus.isMinimizerAt_nodal_truncation_impossible line 665
  33. lemma OAI.CubicTorus.sibling_directionalNormalScalar_mean_zero line 758
  34. lemma OAI.CubicTorus.isMinimizerAt_trace_has_negative line 766
  35. lemma OAI.CubicTorus.isMinimizerAt_negative_unused_patch line 790