OAI/Geometry/CubicTorus/Reflection/TorusCylinders.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.periodic_complete_cylinder_radius_lt_half line 13
  2. theorem OAI.CubicTorus.periodic_connected_cylindrical_boundary line 86
  3. theorem OAI.CubicTorus.isMinimizerAt_axial_curvature_ne_zero line 161
  4. theorem OAI.CubicTorus.isMinimizerAt_zero_coordinate_cylindrical line 208
  5. def OAI.CubicTorus.torusAxialProjection line 263
  6. lemma OAI.CubicTorus.torusAxialProjection_apply line 266
  7. lemma OAI.CubicTorus.torusAxialProjection_continuous line 269
  8. lemma OAI.CubicTorus.torusAxialProjection_zero line 277
  9. lemma OAI.CubicTorus.torusAxialProjection_sub line 279
  10. lemma OAI.CubicTorus.quotientMap_axialProjection line 284
  11. lemma OAI.CubicTorus.norm_transverse_shortestLift line 290
  12. lemma OAI.CubicTorus.quotientMap_image_small_cylinder line 303
  13. def OAI.CubicTorus.axialTube line 322
  14. def OAI.CubicTorus.axialTubeExterior line 325
  15. lemma OAI.CubicTorus.isOpen_axialTube line 328
  16. lemma OAI.CubicTorus.isOpen_axialTubeExterior line 331
  17. lemma OAI.CubicTorus.axialTube_zero_preconnected line 346
  18. lemma OAI.CubicTorus.axialTubeExterior_zero_preconnected line 366
  19. lemma OAI.CubicTorus.axialTube_preconnected line 456
  20. lemma OAI.CubicTorus.axialTubeExterior_preconnected line 463
  21. theorem OAI.CubicTorus.isMinimizerAt_cylindrical_boundary_phase line 482
  22. lemma OAI.CubicTorus.torusCoordinatePermute_apply line 558
  23. lemma OAI.CubicTorus.torusCoordinatePermute_inverse line 561
  24. lemma OAI.CubicTorus.torusCoordinatePermute_measurePreserving line 564
  25. def OAI.CubicTorus.coverCoordinatePermute line 573
  26. lemma OAI.CubicTorus.coverCoordinatePermute_apply line 576
  27. lemma OAI.CubicTorus.coverCoordinatePermute_inverse line 579
  28. lemma OAI.CubicTorus.quotientMap_coordinatePermute line 582
  29. lemma OAI.CubicTorus.coverCoordinatePermute_lattice line 585
  30. lemma OAI.CubicTorus.coverCoordinatePermute_single line 588
  31. def OAI.CubicTorus.coordinatePermutedField line 604
  32. lemma OAI.CubicTorus.coordinatePermutedField_contDiff line 607
  33. lemma OAI.CubicTorus.coordinatePermutedField_periodic line 612
  34. lemma OAI.CubicTorus.coordinatePermutedField_admissible line 618
  35. lemma OAI.CubicTorus.coordinatePermutedField_divergence line 624
  36. lemma OAI.CubicTorus.flux_coordinatePermute line 653
  37. lemma OAI.CubicTorus.perimeter_coordinatePermute_le line 675
  38. lemma OAI.CubicTorus.perimeter_coordinatePermute_measurable line 685
  39. theorem OAI.CubicTorus.perimeter_coordinatePermute line 693
  40. lemma OAI.CubicTorus.volume_coordinatePermute line 701
  41. lemma OAI.CubicTorus.torusCoordinatePermute_norm line 718
  42. lemma OAI.CubicTorus.torusAxialProjection_permute line 724
  43. lemma OAI.CubicTorus.axialTube_zero_model line 735
  44. lemma OAI.CubicTorus.axialTube_eq_permute line 741
  45. lemma OAI.CubicTorus.axialTube_eq_translate line 752
  46. lemma OAI.CubicTorus.axialTube_volume line 757
  47. lemma OAI.CubicTorus.axialTube_perimeter line 763
  48. lemma OAI.CubicTorus.small_minimizer_tube_phase line 783
  49. lemma OAI.CubicTorus.axialTube_isometric_model line 809
  50. theorem OAI.CubicTorus.isMinimizerAt_cylindrical_standard_tube line 832