OAI/Geometry/CubicTorus/Reflection/CoordinateReflection.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicTorus.coordinateReflection line 13
  2. lemma OAI.CubicTorus.coordinateReflection_apply line 16
  3. lemma OAI.CubicTorus.coordinateReflection_involutive line 19
  4. lemma OAI.CubicTorus.coordinateReflection_isometry line 24
  5. def OAI.CubicTorus.coordinateReflectionEquiv line 34
  6. lemma OAI.CubicTorus.coordinateReflection_continuous line 41
  7. lemma OAI.CubicTorus.coordinateReflection_measurePreserving line 44
  8. def OAI.CubicTorus.coverCoordinateReflection line 56
  9. lemma OAI.CubicTorus.coverCoordinateReflection_apply line 60
  10. lemma OAI.CubicTorus.coverCoordinateReflection_involutive line 65
  11. lemma OAI.CubicTorus.quotientMap_coordinateReflection line 70
  12. lemma OAI.CubicTorus.coverCoordinateReflection_lattice line 75
  13. lemma OAI.CubicTorus.coverCoordinateReflection_single line 80
  14. def OAI.CubicTorus.coordinateReflectedField line 103
  15. lemma OAI.CubicTorus.coordinateReflectedField_contDiff line 106
  16. lemma OAI.CubicTorus.coordinateReflectedField_periodic line 111
  17. lemma OAI.CubicTorus.coordinateReflectedField_admissible line 117
  18. lemma OAI.CubicTorus.coordinateReflectedField_divergence line 123
  19. def OAI.CubicTorus.coordinateEvenField line 142
  20. lemma OAI.CubicTorus.coordinateEvenField_admissible line 145
  21. lemma OAI.CubicTorus.coordinateEvenField_reflection line 159
  22. lemma OAI.CubicTorus.coordinateEvenField_divergence line 165
  23. lemma OAI.CubicTorus.flux_coordinateReflection line 186
  24. lemma OAI.CubicTorus.perimeter_coordinateReflection_le line 205
  25. lemma OAI.CubicTorus.perimeter_coordinateReflection_measurable line 215
  26. theorem OAI.CubicTorus.perimeter_coordinateReflection line 223
  27. def OAI.CubicTorus.reflectionCompetitor line 243
  28. lemma OAI.CubicTorus.reflectionCompetitor_measurable line 246
  29. lemma OAI.CubicTorus.reflectionCompetitor_disjoint_parts line 250
  30. lemma OAI.CubicTorus.reflectionCompetitor_volume line 255
  31. lemma OAI.CubicTorus.reflectionCompetitor_realVolume line 263
  32. lemma OAI.CubicTorus.reflectionCompetitor_flux line 269
  33. lemma OAI.CubicTorus.sublevelCutoff_direction_zero line 312
  34. lemma OAI.CubicTorus.sublevelCutoff_direction_bound line 318
  35. lemma OAI.CubicTorus.sublevelCutoff_direction_tendsto line 339
  36. lemma OAI.CubicTorus.sublevelCutoff_direction_integral_tendsto line 351
  37. theorem OAI.CubicTorus.normalMeasure_tangential_sublevel_flux line 385
  38. lemma OAI.CubicTorus.halfInteger_distance_le_sine line 458
  39. def OAI.CubicTorus.coordinateSine line 482
  40. lemma OAI.CubicTorus.coordinateSine_contDiff line 484
  41. lemma OAI.CubicTorus.coordinateSine_periodic line 487
  42. lemma OAI.CubicTorus.coordinateSine_reflection line 495
  43. lemma OAI.CubicTorus.coordinateSine_fderiv line 499
  44. lemma OAI.CubicTorus.coordinateSymmetricField_seam line 504
  45. theorem OAI.CubicTorus.coordinateSymmetricField_tangency line 519
  46. lemma OAI.CubicTorus.reflection_sublevel_disjoint line 564
  47. theorem OAI.CubicTorus.reflectionCompetitor_perimeter_le line 578
  48. theorem OAI.CubicTorus.reflectionCompetitor_sine_perimeter_le line 613
  49. theorem OAI.CubicTorus.reflectionCompetitor_negSine_perimeter_le line 623
  50. theorem OAI.CubicTorus.isMinimizerAt_reflection_competitors line 653
  51. def OAI.CubicTorus.coordinateHalf line 739
  52. lemma OAI.CubicTorus.coordinateHalf_measurable line 742
  53. lemma OAI.CubicTorus.coordinateHalf_seam_zero line 746
  54. lemma OAI.CubicTorus.coordinateHalf_halfturn line 765
  55. lemma OAI.CubicTorus.coordinateHalf_complement_ae line 772
  56. lemma OAI.CubicTorus.coordinateHalf_volume_sum line 785
  57. lemma OAI.CubicTorus.coordinateHalf_volume_continuous line 801
  58. theorem OAI.CubicTorus.exists_coordinateHalf_bisects line 833