OAI/Geometry/CubicTorus/Rigidity/TwoVolumeNodal.lean

GitHub source file

77 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.quotientMap_nsmul line 13
  2. lemma OAI.CubicTorus.torus_same_short_step line 18
  3. lemma OAI.CubicTorus.isometry_straight_step line 34
  4. lemma OAI.CubicTorus.isometry_straight_nsmul line 50
  5. theorem OAI.CubicTorus.torusIsometry_global_linear line 71
  6. theorem OAI.CubicTorus.torusIsometry_lattice_translation line 105
  7. theorem OAI.CubicTorus.torusIsometry_measurePreserving line 122
  8. theorem OAI.CubicTorus.perimeter_torusIsometry line 131
  9. lemma OAI.CubicTorus.finitePerimeter_torusIsometry line 142
  10. theorem OAI.CubicTorus.isMinimizerAt_torusIsometry line 147
  11. lemma OAI.CubicTorus.isometry_image_eq_symm_preimage line 167
  12. theorem OAI.CubicTorus.CongruentAE.symm line 176
  13. lemma OAI.CubicTorus.CongruentAE.nullMeasurableSet line 184
  14. theorem OAI.CubicTorus.CongruentAE.perimeter_eq line 190
  15. theorem OAI.CubicTorus.CongruentAE.volume_eq line 195
  16. theorem OAI.CubicTorus.CongruentAE.isMinimizerAt line 201
  17. theorem OAI.CubicTorus.CongruentAE.isMinimizerAt_iff line 207
  18. theorem OAI.CubicTorus.stripe_congruentAE_slab line 211
  19. lemma OAI.CubicTorus.perimeter_canonicalSlab_le line 242
  20. lemma OAI.CubicTorus.finitePerimeter_canonicalSlab line 248
  21. def OAI.CubicTorus.TwoVolume.sphereArea line 266
  22. def OAI.CubicTorus.TwoVolume.tubeArea line 267
  23. def OAI.CubicTorus.TwoVolume.V₁ line 268
  24. def OAI.CubicTorus.TwoVolume.V₂ line 269
  25. def OAI.CubicTorus.TwoVolume.envelope line 271
  26. lemma OAI.CubicTorus.TwoVolume.transitions line 275
  27. lemma OAI.CubicTorus.TwoVolume.sphereArea_nonneg line 288
  28. lemma OAI.CubicTorus.TwoVolume.sphereArea_pos line 292
  29. lemma OAI.CubicTorus.TwoVolume.sphereArea_cube line 296
  30. lemma OAI.CubicTorus.TwoVolume.tubeArea_sq line 306
  31. lemma OAI.CubicTorus.TwoVolume.sphereArea_le_tubeArea_iff line 309
  32. lemma OAI.CubicTorus.TwoVolume.tubeArea_le_one_iff line 331
  33. lemma OAI.CubicTorus.TwoVolume.sphereArea_zero line 336
  34. lemma OAI.CubicTorus.TwoVolume.tubeArea_zero line 337
  35. lemma OAI.CubicTorus.TwoVolume.tubeArea_nonneg line 338
  36. lemma OAI.CubicTorus.TwoVolume.tubeArea_pos line 339
  37. lemma OAI.CubicTorus.TwoVolume.sphereArea_eq_tubeArea_V₁ line 342
  38. lemma OAI.CubicTorus.TwoVolume.tubeArea_V₂ line 353
  39. lemma OAI.CubicTorus.TwoVolume.envelope_compl line 356
  40. lemma OAI.CubicTorus.TwoVolume.envelope_sphere line 359
  41. lemma OAI.CubicTorus.TwoVolume.envelope_tube line 369
  42. lemma OAI.CubicTorus.TwoVolume.envelope_constant line 381
  43. lemma OAI.CubicTorus.TwoVolume.envelope_zero line 396
  44. lemma OAI.CubicTorus.TwoVolume.envelope_one line 399
  45. lemma OAI.CubicTorus.TwoVolume.continuous_sphereArea line 402
  46. lemma OAI.CubicTorus.TwoVolume.continuous_tubeArea line 405
  47. lemma OAI.CubicTorus.TwoVolume.continuous_envelope line 408
  48. lemma OAI.CubicTorus.TwoVolume.envelope_pos line 412
  49. lemma OAI.CubicTorus.TwoVolume.ode_power line 416
  50. lemma OAI.CubicTorus.TwoVolume.smooth_sphereArea line 425
  51. lemma OAI.CubicTorus.TwoVolume.ode_sphereArea line 428
  52. lemma OAI.CubicTorus.TwoVolume.tubeArea_power line 433
  53. lemma OAI.CubicTorus.TwoVolume.smooth_tubeArea line 437
  54. lemma OAI.CubicTorus.TwoVolume.ode_tubeArea line 441
  55. lemma OAI.CubicTorus.TwoVolume.ode_eventuallyEq line 445
  56. lemma OAI.CubicTorus.TwoVolume.smooth_ode_sphere line 449
  57. lemma OAI.CubicTorus.TwoVolume.smooth_ode_tube line 456
  58. lemma OAI.CubicTorus.TwoVolume.smooth_ode_constant line 463
  59. lemma OAI.CubicTorus.TwoVolume.candidateProfile_eq_two_envelope line 471
  60. theorem OAI.CubicTorus.TwoVolume.two_volume_comparison line 483
  61. lemma OAI.CubicTorus.TwoVolume.smooth_ode_lower line 526
  62. theorem OAI.CubicTorus.TwoVolume.exclude_negative_support_lower line 536
  63. lemma OAI.CubicTorus.canonicalBall_radius_lt line 558
  64. lemma OAI.CubicTorus.canonicalTube_radius_lt line 567
  65. theorem OAI.CubicTorus.perimeter_canonicalBall_eq line 574
  66. theorem OAI.CubicTorus.perimeter_canonicalTube_eq line 580
  67. theorem OAI.CubicTorus.perimeter_canonicalSlab_eq line 589
  68. lemma OAI.CubicTorus.unit_sphereArea line 635
  69. lemma OAI.CubicTorus.candidateProfile_sphere line 646
  70. lemma OAI.CubicTorus.candidateProfile_tube line 650
  71. lemma OAI.CubicTorus.candidateProfile_slab line 655
  72. lemma OAI.CubicTorus.candidateProfile_compl line 659
  73. lemma OAI.CubicTorus.CongruentAE.finitePerimeter line 663
  74. theorem OAI.CubicTorus.SmallStandardRegion.bv_data line 667
  75. theorem OAI.CubicTorus.StandardRegionAt.bv_data line 690
  76. lemma OAI.CubicTorus.isMinimizerAt_iff_profile line 706
  77. theorem OAI.CubicTorus.StandardRegionAt.minimizer_iff line 718