OAI/Geometry/CubicTorus/Estimates/BVRadial.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicTorus.cubeCenter line 16
  2. def OAI.CubicTorus.cubeBall line 18
  3. lemma OAI.CubicTorus.measurableSet_cubeBall line 20
  4. lemma OAI.CubicTorus.coverBall_subset_cube line 23
  5. lemma OAI.CubicTorus.cubeBall_lift line 33
  6. lemma OAI.CubicTorus.volume_cubeBall line 46
  7. def OAI.CubicTorus.radialBump line 53
  8. def OAI.CubicTorus.radialCore line 59
  9. def OAI.CubicTorus.radialSquared line 61
  10. lemma OAI.CubicTorus.radialCore_contDiff line 63
  11. lemma OAI.CubicTorus.radialCore_compactSupport line 66
  12. lemma OAI.CubicTorus.radialCore_tsupport line 69
  13. lemma OAI.CubicTorus.radialSquared_contDiff line 80
  14. lemma OAI.CubicTorus.radialSquared_periodic line 83
  15. lemma OAI.CubicTorus.radialSquared_eq_on_cube line 87
  16. lemma OAI.CubicTorus.radialSquared_eventuallyEq_norm_sq line 94
  17. lemma OAI.CubicTorus.radialSquared_sublevel_iff line 106
  18. lemma OAI.CubicTorus.representative_mem_fundamentalCube line 129
  19. lemma OAI.CubicTorus.sublevelRegion_radialSquared line 133
  20. lemma OAI.CubicTorus.norm_gradient_radialSquared_of_mem_cube line 141
  21. lemma OAI.CubicTorus.norm_gradient_radialSquared line 160
  22. lemma OAI.CubicTorus.dist_representative_cubeCenter line 172
  23. lemma OAI.CubicTorus.cubeBall_eq_metricBall line 192
  24. lemma OAI.CubicTorus.centeredBall_eq_cubeBall_preimage line 198
  25. lemma OAI.CubicTorus.volume_centeredBall line 205
  26. lemma OAI.CubicTorus.volume_torusBall line 210
  27. def OAI.CubicTorus.localRadialSquared line 217
  28. lemma OAI.CubicTorus.localRadialSquared_contDiff line 220
  29. lemma OAI.CubicTorus.localRadialSquared_periodic line 224
  30. lemma OAI.CubicTorus.sublevelRegion_localRadialSquared line 231
  31. lemma OAI.CubicTorus.norm_gradient_localRadialSquared line 244
  32. lemma OAI.CubicTorus.sublevelVolume_localRadialSquared_le line 255
  33. theorem OAI.CubicTorus.monotone_density_root_lower line 281
  34. theorem OAI.CubicTorus.monotone_density_lower line 351
  35. theorem OAI.CubicTorus.isMinimizerAt_volume_density line 379
  36. def OAI.CubicTorus.volumeSupport line 464
  37. lemma OAI.CubicTorus.mem_volumeSupport_iff line 466
  38. lemma OAI.CubicTorus.isClosed_volumeSupport line 474
  39. lemma OAI.CubicTorus.volumeSupport_union_compl line 477
  40. theorem OAI.CubicTorus.isMinimizerAt_two_sided_density line 482
  41. instance OAI.CubicTorus.torusVolume_doubling line 500
  42. lemma OAI.CubicTorus.realVolume_closedBall_le line 518
  43. lemma OAI.CubicTorus.setIntegral_characteristic line 528
  44. lemma OAI.CubicTorus.volumeSupport_ae_eq_of_density line 535
  45. def OAI.CubicTorus.openRepresentative line 582
  46. lemma OAI.CubicTorus.isOpen_openRepresentative line 584
  47. theorem OAI.CubicTorus.isMinimizerAt_openRepresentative_ae line 587
  48. lemma OAI.CubicTorus.volumeSupport_congr_ae line 597
  49. lemma OAI.CubicTorus.volumeSupport_eq_closure line 602
  50. lemma OAI.CubicTorus.isMinimizerAt_closure_openRepresentative line 611
  51. lemma OAI.CubicTorus.isMinimizerAt_frontier_openRepresentative line 617
  52. theorem OAI.CubicTorus.isMinimizerAt_volume_frontier_eq_zero line 624
  53. theorem OAI.CubicTorus.isMinimizerAt_exists_open_density_representative line 641
  54. def OAI.CubicTorus.normalProjection line 678
  55. lemma OAI.CubicTorus.normalProjection_continuous line 680
  56. def OAI.CubicTorus.spatialNormalMeasure line 683
  57. lemma OAI.CubicTorus.integral_spatialNormalMeasure line 686
  58. lemma OAI.CubicTorus.integral_spatialNormalMeasure_periodic line 693
  59. lemma OAI.CubicTorus.spatialNormalMeasure_weightedPerimeter line 704
  60. lemma OAI.CubicTorus.sublevelCutoff_eq_zero line 712
  61. lemma OAI.CubicTorus.sublevelCutoff_eq_one line 716
  62. lemma OAI.CubicTorus.divergence_cutoff_zero line 721
  63. lemma OAI.CubicTorus.admissible_sublevelCutoff line 730
  64. lemma OAI.CubicTorus.weightedPerimeter_sublevelCutoff_le line 738
  65. lemma OAI.CubicTorus.spatialNormalMeasure_sublevel_le line 763
  66. lemma OAI.CubicTorus.monotone_exists_deriv_le line 814
  67. theorem OAI.CubicTorus.isMinimizerAt_perimeter_upper_density line 832