OAI/Geometry/CubicTorus/Profiles/NormalMap.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.LatticeIsometry.volumeSupport_preimage line 14
  2. lemma OAI.CubicTorus.LatticeIsometry.openRepresentative_preimage line 28
  3. lemma OAI.CubicTorus.LatticeIsometry.frontier_openRepresentative_preimage line 34
  4. def OAI.CubicTorus.LatticeIsometry.normalMap line 40
  5. lemma OAI.CubicTorus.LatticeIsometry.measurable_normalMap line 44
  6. lemma OAI.CubicTorus.LatticeIsometry.normalMap_periodic_eval line 51
  7. lemma OAI.CubicTorus.LatticeIsometry.isNormalMeasure_preimage line 57
  8. lemma OAI.CubicTorus.LatticeIsometry.pullback_normal_ae line 81
  9. theorem OAI.CubicTorus.LatticeIsometry.normal_equivariant line 97
  10. def OAI.CubicTorus.axisReflection line 128
  11. lemma OAI.CubicTorus.axisReflection_cover_apply line 139
  12. lemma OAI.CubicTorus.axisReflection_torus_apply line 154
  13. lemma OAI.CubicTorus.axisReflection_conjugate line 169
  14. def OAI.CubicTorus.centeredAxisReflection line 182
  15. lemma OAI.CubicTorus.centeredAxisReflection_apply line 186
  16. lemma OAI.CubicTorus.centeredAxisReflection_eq line 193
  17. lemma OAI.CubicTorus.translated_axis_symmetry_iff line 201
  18. lemma OAI.CubicTorus.axisReflection_zero_torus line 231
  19. lemma OAI.CubicTorus.torusCoordinateSwap_involutive line 235
  20. lemma OAI.CubicTorus.centeredAxisReflection_conjugate line 241
  21. theorem OAI.CubicTorus.isMinimizerAt_exists_axis_reflection line 255
  22. theorem OAI.CubicTorus.isMinimizerAt_common_reflection_origin line 281
  23. lemma OAI.CubicTorus.representative_coordinatePermute line 316
  24. lemma OAI.CubicTorus.LatticeIsometry.pullback_representative line 321
  25. lemma OAI.CubicTorus.coordinateSwap_pullback_scalar line 329
  26. theorem OAI.CubicTorus.isMinimizerAt_axis_strict_normal_sign line 340
  27. theorem OAI.CubicTorus.isMinimizerAt_zero_axis_standard line 418
  28. theorem OAI.CubicTorus.isMinimizerAt_nonstandard_axis_strict_normal_sign line 448
  29. theorem OAI.CubicTorus.normalMeasure_signed_translation line 485
  30. lemma OAI.CubicTorus.periodic_descent_translate line 554
  31. theorem OAI.CubicTorus.isMinimizerAt_test_phase_propagation line 561
  32. lemma OAI.CubicTorus.latticePeriodize_ne_zero line 635
  33. theorem OAI.CubicTorus.isMinimizerAt_convex_phase_monotone line 641
  34. def OAI.CubicTorus.upperOctant line 736
  35. lemma OAI.CubicTorus.isOpen_upperOctant line 738
  36. lemma OAI.CubicTorus.convex_upperOctant line 744
  37. def OAI.CubicTorus.OrientedCoordinateLE line 751
  38. lemma OAI.CubicTorus.isMinimizerAt_octant_normal_orientation line 754
  39. theorem OAI.CubicTorus.isMinimizerAt_octant_downset line 787
  40. lemma OAI.CubicTorus.isMinimizerAt_axis_fixed_normal_zero line 831