OAI/Geometry/CubicTorus/Regularity/SmoothApproxLip.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.characteristic_dichotomy line 13
  2. lemma OAI.CubicTorus.characteristic_bound line 18
  3. lemma OAI.CubicTorus.setIntegral_lift_measurable line 21
  4. lemma OAI.CubicTorus.torus_test_translation_bound line 29
  5. lemma OAI.CubicTorus.integral_difference_test line 43
  6. theorem OAI.CubicTorus.characteristic_translation_bound line 85
  7. def OAI.CubicTorus.smoothApproxLip line 111
  8. lemma OAI.CubicTorus.smoothApprox_lipschitz line 115
  9. lemma OAI.CubicTorus.quotientMap_sub line 147
  10. def OAI.CubicTorus.torusApprox line 150
  11. lemma OAI.CubicTorus.torusApprox_measurable line 153
  12. lemma OAI.CubicTorus.torusApprox_bound line 159
  13. lemma OAI.CubicTorus.torusApprox_integrable line 162
  14. lemma OAI.CubicTorus.integrable_characteristic line 167
  15. lemma OAI.CubicTorus.torusApprox_sub_eq_integral line 170
  16. theorem OAI.CubicTorus.torusApprox_error line 185
  17. def OAI.CubicTorus.closedFundamentalCube line 257
  18. lemma OAI.CubicTorus.isCompact_closedFundamentalCube line 260
  19. abbrev OAI.CubicTorus.CompactCell line 263
  20. instance OAI.CubicTorus.(instance at line 265) line 265
  21. lemma OAI.CubicTorus.representative_mem_closedCube line 267
  22. def OAI.CubicTorus.cubeRepresentative line 275
  23. lemma OAI.CubicTorus.measurable_cubeRepresentative line 277
  24. lemma OAI.CubicTorus.integrable_cubeEval line 280
  25. def OAI.CubicTorus.cubeToL1 line 285
  26. lemma OAI.CubicTorus.cubeToL1_lipschitz line 288
  27. def OAI.CubicTorus.characteristicL1 line 306
  28. def OAI.CubicTorus.torusApproxL1 line 309
  29. lemma OAI.CubicTorus.dist_torusApproxL1 line 312
  30. lemma OAI.CubicTorus.totallyBounded_torusApproxL1 line 325
  31. lemma OAI.CubicTorus.totallyBounded_characteristicL1 line 359
  32. theorem OAI.CubicTorus.exists_ae_tendsto_characteristic line 391
  33. def OAI.CubicTorus.stripe line 429
  34. def OAI.CubicTorus.stripeUpper line 432
  35. lemma OAI.CubicTorus.measurableSet_stripe line 434
  36. lemma OAI.CubicTorus.stripe_lift_preimage line 439
  37. lemma OAI.CubicTorus.volume_stripe line 468
  38. lemma OAI.CubicTorus.integral_divergence_stripe line 478
  39. lemma OAI.CubicTorus.volume_square_face line 544
  40. lemma OAI.CubicTorus.stripe_flux_bound line 548
  41. theorem OAI.CubicTorus.perimeter_stripe_le line 557
  42. theorem OAI.CubicTorus.finitePerimeter_stripe line 571
  43. theorem OAI.CubicTorus.exists_bounded_competitor line 574
  44. theorem OAI.CubicTorus.exists_isMinimizerAt line 584
  45. lemma OAI.CubicTorus.characteristic_translation_ae_of_perimeter_zero line 625
  46. theorem OAI.CubicTorus.volume_eq_zero_or_one_of_perimeter_zero line 643
  47. theorem OAI.CubicTorus.perimeter_pos_of_volume line 673
  48. def OAI.CubicTorus.isoperimetricProfile line 692
  49. lemma OAI.CubicTorus.isoperimetricProfile_eq_of_isMinimizerAt line 696
  50. lemma OAI.CubicTorus.isMinimizerAt_empty line 707
  51. lemma OAI.CubicTorus.isMinimizerAt_univ line 713
  52. theorem OAI.CubicTorus.exists_isMinimizerAt_Icc line 717
  53. lemma OAI.CubicTorus.isoperimetricProfile_nonneg line 727
  54. lemma OAI.CubicTorus.isoperimetricProfile_zero line 730
  55. lemma OAI.CubicTorus.isoperimetricProfile_one line 734
  56. lemma OAI.CubicTorus.isoperimetricProfile_pos line 740
  57. lemma OAI.CubicTorus.isoperimetricProfile_le_competitor line 747
  58. lemma OAI.CubicTorus.isoperimetricProfile_le_one line 754
  59. lemma OAI.CubicTorus.isoperimetricProfile_compl line 761
  60. lemma OAI.CubicTorus.isClosed_profile_sublevel line 774
  61. theorem OAI.CubicTorus.lowerSemicontinuousOn_isoperimetricProfile line 812
  62. lemma OAI.CubicTorus.integrableOn_periodic_continuous line 827
  63. lemma OAI.CubicTorus.divergence_smul_function line 834
  64. lemma OAI.CubicTorus.admissible_cutoff line 853
  65. lemma OAI.CubicTorus.gradient_contDiff line 865
  66. lemma OAI.CubicTorus.gradient_periodic line 870