OAI/Geometry/CubicTorus/Reflection/NormalMeasureCoordinateReflection.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.volumeSupport_local_mono line 13
  2. lemma OAI.CubicTorus.volumeSupport_local_eq line 24
  3. lemma OAI.CubicTorus.openRepresentative_local_eq line 31
  4. lemma OAI.CubicTorus.isMinimizerAt_frontier_local_eq line 44
  5. lemma OAI.CubicTorus.local_region_flux_eq line 64
  6. lemma OAI.CubicTorus.local_region_weightedPerimeter_eq line 85
  7. lemma OAI.CubicTorus.local_region_weighted_mass_eq line 111
  8. theorem OAI.CubicTorus.isMinimizerAt_normal_local_eq line 126
  9. theorem OAI.CubicTorus.isMinimizerAt_connected_of_shared_patch line 205
  10. theorem OAI.CubicTorus.isMinimizerAt_boundary_eq_of_shared_patch line 255
  11. lemma OAI.CubicTorus.local_replace_ae line 293
  12. lemma OAI.CubicTorus.local_replace_inter line 302
  13. lemma OAI.CubicTorus.openRepresentative_local_ae_eq line 307
  14. lemma OAI.CubicTorus.isMinimizerAt_normal_local_ae_eq line 313
  15. lemma OAI.CubicTorus.quotient_chart_ae line 329
  16. theorem OAI.CubicTorus.isMinimizerAt_centered_common_boundary_phases line 355
  17. theorem OAI.CubicTorus.isMinimizerAt_common_boundary_phases line 433
  18. lemma OAI.CubicTorus.normal_reverse_ae line 475
  19. theorem OAI.CubicTorus.isMinimizerAt_oriented_boundary_local_ae line 483
  20. lemma OAI.CubicTorus.sets_eq_of_common_frontier_local_eq line 532
  21. theorem OAI.CubicTorus.isMinimizerAt_region_eq_of_shared_patch line 569
  22. lemma OAI.CubicTorus.isMinimizerAt_two_phase_frontier line 599
  23. theorem OAI.CubicTorus.isMinimizerAt_reflection_symmetry_of_competitor line 615
  24. theorem OAI.CubicTorus.isMinimizerAt_exists_coordinate_reflection_measurable line 648
  25. theorem OAI.CubicTorus.isMinimizerAt_exists_coordinate_reflection line 661
  26. lemma OAI.CubicTorus.coordinateReflection_add line 691
  27. lemma OAI.CubicTorus.coordinateReflection_coordinate_shift line 696
  28. lemma OAI.CubicTorus.reflection_invariance_translation line 707
  29. theorem OAI.CubicTorus.isMinimizerAt_exists_coordinate_symmetries_measurable line 717
  30. theorem OAI.CubicTorus.isMinimizerAt_slab_or_coordinate_symmetries line 750
  31. def OAI.CubicTorus.reflectNormal line 783
  32. lemma OAI.CubicTorus.measurable_reflectNormal line 787
  33. lemma OAI.CubicTorus.reflectNormal_periodic_eval line 794
  34. lemma OAI.CubicTorus.coverCoordinateReflection_inner line 801
  35. theorem OAI.CubicTorus.isNormalMeasure_coordinateReflection line 806
  36. lemma OAI.CubicTorus.reflected_normal_ae line 828
  37. theorem OAI.CubicTorus.isMinimizerAt_normal_reflection line 846