OAI/Geometry/CubicTorus/Profiles/FirstSeamFunction.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.coverAEAgreement_common_model line 13
  2. lemma OAI.CubicTorus.off_essential_boundary_phase line 26
  3. lemma OAI.CubicTorus.graph_boundary_local_phase line 38
  4. theorem OAI.CubicTorus.graph_boundary_phase_identity line 61
  5. theorem OAI.CubicTorus.isMinimizerAt_same_boundary_phase line 92
  6. theorem OAI.CubicTorus.isMinimizerAt_connected_common_patch line 121
  7. lemma OAI.CubicTorus.normalized_CMC_oriented_germ_curvature line 149
  8. theorem OAI.CubicTorus.normalized_CMC_common_germ_curvature line 184
  9. theorem OAI.CubicTorus.isMinimizerAt_connected_of_common_patch line 223
  10. theorem OAI.CubicTorus.isMinimizerAt_common_patch_rigidity line 248
  11. lemma OAI.CubicTorus.isMinimizerAt_boundary_local_ae line 271
  12. lemma OAI.CubicTorus.connected_torus_phase line 287
  13. lemma OAI.CubicTorus.isMinimizerAt_boundary_meets_region line 317
  14. theorem OAI.CubicTorus.isMinimizerAt_local_region_rigidity line 330
  15. def OAI.CubicTorus.firstSeamFunction line 366
  16. lemma OAI.CubicTorus.firstSeamFunction_contDiff line 368
  17. lemma OAI.CubicTorus.firstSeamFunction_periodic line 373
  18. lemma OAI.CubicTorus.firstSeamFunction_reflection line 382
  19. lemma OAI.CubicTorus.firstSeam_distance_bound line 386
  20. lemma OAI.CubicTorus.smooth_periodic_lipschitz line 408
  21. lemma OAI.CubicTorus.reflection_symmetric_seam_zero line 416
  22. lemma OAI.CubicTorus.reflection_symmetric_seam_bound line 433
  23. lemma OAI.CubicTorus.fderiv_firstSeamFunction line 473
  24. lemma OAI.CubicTorus.seam_cutoff_error_bound line 482
  25. lemma OAI.CubicTorus.seam_cutoff_error_tendsto line 509
  26. lemma OAI.CubicTorus.reflectionPullback_sub line 528
  27. lemma OAI.CubicTorus.seam_cutoff_integral_error_tendsto line 534
  28. theorem OAI.CubicTorus.symmetric_partition_flux_le line 559
  29. lemma OAI.CubicTorus.firstSeam_representative_reflection line 626
  30. lemma OAI.CubicTorus.firstSeam_null line 633
  31. def OAI.CubicTorus.reflectionClosure line 654
  32. lemma OAI.CubicTorus.measurableSet_reflectionClosure line 657
  33. lemma OAI.CubicTorus.reflected_half_disjoint line 661
  34. lemma OAI.CubicTorus.reflected_other_half_aedisjoint line 671
  35. lemma OAI.CubicTorus.lift_aedisjoint line 682
  36. lemma OAI.CubicTorus.flux_union_ae line 695
  37. def OAI.CubicTorus.reflectionMean line 706
  38. lemma OAI.CubicTorus.reflectionMean_admissible line 709
  39. lemma OAI.CubicTorus.reflectionMean_symmetric line 716
  40. lemma OAI.CubicTorus.divergence_reflectionMean line 722
  41. lemma OAI.CubicTorus.flux_reflectionClosure line 734
  42. lemma OAI.CubicTorus.volume_reflectionClosure line 748
  43. lemma OAI.CubicTorus.perimeter_pair_le_of_flux_bound line 769
  44. theorem OAI.CubicTorus.reflected_halves_perimeter_bound line 793
  45. lemma OAI.CubicTorus.volume_halves_sum line 811
  46. theorem OAI.CubicTorus.bisected_reflection_minimizers line 818