OAI/Geometry/CubicTorus/Regularity/BVRegularity.lean

GitHub source file

84 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.continuous_quotientMap line 20
  2. lemma OAI.CubicTorus.measurable_quotientMap line 24
  3. lemma OAI.CubicTorus.measurableSet_fundamentalCube line 26
  4. lemma OAI.CubicTorus.volume_fundamentalCube line 34
  5. lemma OAI.CubicTorus.torusVolume_univ line 46
  6. instance OAI.CubicTorus.(instance at line 50) line 50
  7. lemma OAI.CubicTorus.admissible_zero line 52
  8. lemma OAI.CubicTorus.divergence_zero line 55
  9. lemma OAI.CubicTorus.admissible_neg line 58
  10. lemma OAI.CubicTorus.divergence_neg line 67
  11. lemma OAI.CubicTorus.perimeter_empty line 74
  12. lemma OAI.CubicTorus.finitePerimeter_empty line 77
  13. lemma OAI.CubicTorus.liftSet_congr_ae line 80
  14. theorem OAI.CubicTorus.perimeter_congr_ae line 93
  15. theorem OAI.CubicTorus.finitePerimeter_congr_ae line 102
  16. theorem OAI.CubicTorus.isMinimizerAt_congr_ae line 107
  17. lemma OAI.CubicTorus.continuous_divergence line 112
  18. lemma OAI.CubicTorus.cube_preimage line 120
  19. lemma OAI.CubicTorus.integrableOn_divergence line 125
  20. lemma OAI.CubicTorus.adjacent_faces line 136
  21. theorem OAI.CubicTorus.integral_divergence_fundamentalCube line 144
  22. lemma OAI.CubicTorus.quotientMap_measurePreserving line 187
  23. lemma OAI.CubicTorus.integral_divergence_compl line 191
  24. theorem OAI.CubicTorus.perimeter_compl line 203
  25. theorem OAI.CubicTorus.finitePerimeter_compl line 218
  26. def OAI.CubicTorus.characteristic line 227
  27. lemma OAI.CubicTorus.lift_indicator_integral line 229
  28. lemma OAI.CubicTorus.characteristic_mul line 236
  29. theorem OAI.CubicTorus.tendsto_lift_integral line 241
  30. theorem OAI.CubicTorus.perimeter_le_of_ae_tendsto line 263
  31. lemma OAI.CubicTorus.integral_characteristic line 282
  32. theorem OAI.CubicTorus.tendsto_volume_of_ae_tendsto line 288
  33. lemma OAI.CubicTorus.volume_compl_of_volume line 308
  34. theorem OAI.CubicTorus.isMinimizerAt_compl line 315
  35. theorem OAI.CubicTorus.perimeter_le_of_ae_tendsto_bound line 333
  36. abbrev OAI.CubicTorus.ProductTorus line 358
  37. lemma OAI.CubicTorus.circle_measurePreserving_mk_Ico line 360
  38. lemma OAI.CubicTorus.torusVolume_eq_product line 366
  39. lemma OAI.CubicTorus.product_to_torus_measurePreserving line 385
  40. lemma OAI.CubicTorus.torus_to_product_measurePreserving line 390
  41. instance OAI.CubicTorus.circle_probability line 395
  42. lemma OAI.CubicTorus.torus_coordinate_measurePreserving line 399
  43. lemma OAI.CubicTorus.measurableSet_canonicalSlab line 404
  44. lemma OAI.CubicTorus.volume_canonicalSlab line 407
  45. instance OAI.CubicTorus.torusVolume_haar line 422
  46. lemma OAI.CubicTorus.quotientMap_add line 428
  47. lemma OAI.CubicTorus.quotientMap_neg line 432
  48. def OAI.CubicTorus.representative line 436
  49. lemma OAI.CubicTorus.measurable_representative line 439
  50. lemma OAI.CubicTorus.quotientMap_representative line 446
  51. lemma OAI.CubicTorus.quotientMap_surjective line 450
  52. lemma OAI.CubicTorus.same_quotient_lattice line 453
  53. lemma OAI.CubicTorus.periodic_representative line 467
  54. lemma OAI.CubicTorus.divergence_translate line 473
  55. lemma OAI.CubicTorus.divergence_periodic line 477
  56. lemma OAI.CubicTorus.admissible_translate line 483
  57. lemma OAI.CubicTorus.setIntegral_lift line 490
  58. lemma OAI.CubicTorus.flux_translation line 503
  59. lemma OAI.CubicTorus.perimeter_translation_le line 534
  60. lemma OAI.CubicTorus.perimeter_translation_measurable line 545
  61. theorem OAI.CubicTorus.perimeter_translation line 558
  62. lemma OAI.CubicTorus.volume_translation line 565
  63. lemma OAI.CubicTorus.finitePerimeter_translation line 569
  64. theorem OAI.CubicTorus.isMinimizerAt_translation line 575
  65. lemma OAI.CubicTorus.divergence_smul_const line 587
  66. lemma OAI.CubicTorus.divergence_const_smul line 600
  67. lemma OAI.CubicTorus.abs_flux_le_perimeter line 607
  68. lemma OAI.CubicTorus.abs_flux_le_mul_perimeter line 621
  69. lemma OAI.CubicTorus.periodic_bounded line 648
  70. lemma OAI.CubicTorus.fderiv_periodic line 664
  71. instance OAI.CubicTorus.finiteMeasure_liftSet line 671
  72. lemma OAI.CubicTorus.abs_directional_flux_le line 679
  73. theorem OAI.CubicTorus.smooth_test_translation_bound line 703
  74. def OAI.CubicTorus.mollifier line 759
  75. lemma OAI.CubicTorus.mollifier_rOut_tendsto line 765
  76. def OAI.CubicTorus.smoothApprox line 770
  77. lemma OAI.CubicTorus.locallyIntegrable_of_bounded line 773
  78. lemma OAI.CubicTorus.smoothApprox_contDiff line 779
  79. lemma OAI.CubicTorus.smoothApprox_bound line 785
  80. lemma OAI.CubicTorus.smoothApprox_periodic line 797
  81. lemma OAI.CubicTorus.smoothApprox_ae_tendsto line 806
  82. theorem OAI.CubicTorus.measurable_test_translation_bound line 819
  83. lemma OAI.CubicTorus.quotientMap_latticeVector line 858
  84. lemma OAI.CubicTorus.measurable_characteristic line 862