OAI/Geometry/CubicTorus/Estimates/LatticeHeightHom.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.complete_planes_normals_parallel line 13
  2. theorem OAI.CubicTorus.Periodic.isMinimizerAt_connected_or_parallel_planes line 71
  3. def OAI.CubicTorus.latticeHeightHom line 103
  4. theorem OAI.CubicTorus.flat_periodic_normal_integral line 108
  5. theorem OAI.CubicTorus.Periodic.isMinimizerAt_connected_or_integral_planes line 175
  6. theorem OAI.CubicTorus.compact_flat_boundary_finite_planes line 212
  7. theorem OAI.CubicTorus.Periodic.isMinimizerAt_connected_or_finite_integral_planes line 253
  8. theorem OAI.CubicTorus.continuous_line_avoids_frontier line 290
  9. theorem OAI.CubicTorus.open_phase_tangent_invariant line 315
  10. theorem OAI.CubicTorus.open_planar_phase_factor line 337
  11. theorem OAI.CubicTorus.Periodic.isMinimizerAt_connected_or_planar_phase line 362
  12. def OAI.CubicTorus.integerCharacter line 410
  13. lemma OAI.CubicTorus.continuous_integerCharacter line 415
  14. lemma OAI.CubicTorus.integerCharacter_quotientMap line 420
  15. lemma OAI.CubicTorus.integerCharacter_surjective line 433
  16. theorem OAI.CubicTorus.integerCharacter_measurePreserving line 448
  17. theorem OAI.CubicTorus.periodic_open_phase_descends line 471
  18. theorem OAI.CubicTorus.Periodic.isMinimizerAt_connected_or_circle_phase line 490
  19. def OAI.CubicTorus.Periodic.simultaneousArea line 532
  20. lemma OAI.CubicTorus.Periodic.simultaneousArea_smoothAt line 535
  21. lemma OAI.CubicTorus.Periodic.simultaneousArea_zero line 540
  22. lemma OAI.CubicTorus.Periodic.simultaneousArea_deriv line 546
  23. theorem OAI.CubicTorus.Periodic.normal_chain_support_jets line 560
  24. theorem OAI.CubicTorus.Periodic.isMinimizerAt_normal_support_jets line 606
  25. theorem OAI.CubicTorus.smooth_linear_volume_correction line 646
  26. theorem OAI.CubicTorus.Periodic.chain_linear_volume_correction line 681
  27. lemma OAI.CubicTorus.Periodic.coordinateCMC_of_global line 718
  28. lemma OAI.CubicTorus.Periodic.correctedChainArea_deriv_zero_speed line 740
  29. lemma OAI.CubicTorus.Periodic.correctedChainArea_second_zero_speed line 773
  30. theorem OAI.CubicTorus.Periodic.isMinimizerAt_affine_volume_support_with_CMC line 795