OAI/Geometry/CubicTorus/Reflection/CoordinateReflection2.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.isMinimizerAt_jensen_projection line 13
  2. theorem OAI.CubicTorus.isMinimizerAt_missing_axis_area_jensen line 49
  3. theorem OAI.CubicTorus.isMinimizerAt_chamber_smooth_exit line 102
  4. theorem OAI.CubicTorus.isMinimizerAt_endpoint_slice_length line 155
  5. theorem OAI.CubicTorus.isMinimizerAt_endpoint_slice_isoperimetric line 201
  6. lemma OAI.CubicTorus.fourCorner_zero_curvature_impossible line 240
  7. theorem OAI.CubicTorus.isMinimizerAt_four_corner_multiplier_ne_zero line 275
  8. theorem OAI.CubicTorus.isMinimizerAt_nonstandard_toroidal_or_corner line 321
  9. theorem OAI.CubicTorus.secondEndpoint_missing_curvature_scalar_witness line 385
  10. def OAI.CubicTorus.firstReflection line 436
  11. lemma OAI.CubicTorus.firstReflection_apply line 440
  12. lemma OAI.CubicTorus.firstReflection_involutive line 445
  13. lemma OAI.CubicTorus.firstReflection_symm line 451
  14. def OAI.CubicTorus.torusFirstReflection line 457
  15. lemma OAI.CubicTorus.torusFirstReflection_apply line 470
  16. lemma OAI.CubicTorus.torusFirstReflection_involutive line 473
  17. lemma OAI.CubicTorus.firstReflection_quotient line 477
  18. lemma OAI.CubicTorus.torusFirstReflection_measurePreserving line 483
  19. lemma OAI.CubicTorus.firstReflection_lattice line 499
  20. def OAI.CubicTorus.reflectionPullback line 506
  21. lemma OAI.CubicTorus.reflectionPullback_contDiff line 509
  22. lemma OAI.CubicTorus.reflectionPullback_periodic line 515
  23. lemma OAI.CubicTorus.reflectionPullback_admissible line 521
  24. lemma OAI.CubicTorus.divergence_reflectionPullback line 526
  25. lemma OAI.CubicTorus.reflectionPullback_involutive line 533
  26. lemma OAI.CubicTorus.flux_firstReflection line 538
  27. lemma OAI.CubicTorus.perimeter_firstReflection line 561
  28. structure OAI.CubicTorus.LatticeIsometry line 585
  29. def OAI.CubicTorus.LatticeIsometry.symm line 592
  30. lemma OAI.CubicTorus.LatticeIsometry.map_zero line 599
  31. lemma OAI.CubicTorus.LatticeIsometry.map_add line 603
  32. def OAI.CubicTorus.LatticeIsometry.addHom line 608
  33. lemma OAI.CubicTorus.LatticeIsometry.measurePreserving line 613
  34. lemma OAI.CubicTorus.LatticeIsometry.lattice line 616
  35. def OAI.CubicTorus.LatticeIsometry.pullback line 624
  36. lemma OAI.CubicTorus.LatticeIsometry.pullback_contDiff line 627
  37. lemma OAI.CubicTorus.LatticeIsometry.pullback_periodic line 631
  38. lemma OAI.CubicTorus.LatticeIsometry.pullback_admissible line 638
  39. lemma OAI.CubicTorus.LatticeIsometry.divergence_pullback line 643
  40. lemma OAI.CubicTorus.LatticeIsometry.flux line 648
  41. lemma OAI.CubicTorus.LatticeIsometry.perimeter_measurable line 671
  42. theorem OAI.CubicTorus.LatticeIsometry.perimeter_eq line 687
  43. lemma OAI.CubicTorus.LatticeIsometry.finitePerimeter line 694
  44. theorem OAI.CubicTorus.LatticeIsometry.isMinimizerAt line 698
  45. def OAI.CubicTorus.centeredIsometryLift line 720
  46. lemma OAI.CubicTorus.norm_quotientMap_of_small line 723
  47. lemma OAI.CubicTorus.centeredIsometryLift_norm line 727
  48. lemma OAI.CubicTorus.centeredIsometryLift_dist line 732
  49. lemma OAI.CubicTorus.centeredIsometryLift_inner line 743
  50. theorem OAI.CubicTorus.torusIsometry_local_linear line 753