OAI/Geometry/CubicTorus/Regularity/BVRadialVariation.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.image_quotientMap_eq_preimage_representative line 15
  2. lemma OAI.CubicTorus.torusVolume_quotientMap_image_cube line 25
  3. lemma OAI.CubicTorus.haar_image_add_right line 42
  4. lemma OAI.CubicTorus.measurableSet_image_add_right line 54
  5. lemma OAI.CubicTorus.image_quotientMap_eq_preimage_shortestLift line 67
  6. lemma OAI.CubicTorus.torusVolume_quotientMap_image_local line 79
  7. lemma OAI.CubicTorus.torusVolume_chart_image line 94
  8. lemma OAI.CubicTorus.quotientMap_chart_image_ball line 102
  9. lemma OAI.CubicTorus.torusVolume_chart_map_restrict line 116
  10. def OAI.CubicTorus.radialDensityWeight line 141
  11. def OAI.CubicTorus.radialDensitySlope line 144
  12. def OAI.CubicTorus.radialDensityField line 147
  13. lemma OAI.CubicTorus.radialDensityWeight_contDiff line 150
  14. lemma OAI.CubicTorus.radialDensityField_contDiff line 154
  15. lemma OAI.CubicTorus.radialDensityWeight_nonneg line 158
  16. lemma OAI.CubicTorus.radialDensitySlope_nonneg line 161
  17. lemma OAI.CubicTorus.radialDensityWeight_zero line 165
  18. lemma OAI.CubicTorus.radialDensitySlope_zero line 170
  19. lemma OAI.CubicTorus.radialDensityField_tsupport line 175
  20. lemma OAI.CubicTorus.radialDensityField_hasCompactSupport line 184
  21. lemma OAI.CubicTorus.fderiv_norm_sq_sub line 188
  22. lemma OAI.CubicTorus.fderiv_radialDensityWeight line 195
  23. lemma OAI.CubicTorus.divergence_sub_const line 207
  24. lemma OAI.CubicTorus.tangentialDivergence_radialDensityField line 211
  25. lemma OAI.CubicTorus.radialDensityField_flux_bound line 227
  26. lemma OAI.CubicTorus.radialDensityField_dilation_bound line 237
  27. def OAI.CubicTorus.radialDensityMass line 264
  28. lemma OAI.CubicTorus.continuous_radialDensitySlope line 267
  29. lemma OAI.CubicTorus.integrable_radialDensityWeight line 273
  30. lemma OAI.CubicTorus.integrable_radialDensitySlope line 279
  31. lemma OAI.CubicTorus.hasDerivAt_radialDensityWeight line 285
  32. lemma OAI.CubicTorus.hasDerivAt_radialDensityMass line 295
  33. lemma OAI.CubicTorus.radialDensityMass_nonneg line 325
  34. theorem OAI.CubicTorus.weakCMC_radialDensityMass_ode line 329
  35. lemma OAI.CubicTorus.hasDerivAt_cmcDensityRatio line 390
  36. theorem OAI.CubicTorus.cmcDensityRatio_monotoneOn line 401
  37. def OAI.CubicTorus.cellBallMass line 428
  38. lemma OAI.CubicTorus.measurableSet_cellBall line 431
  39. lemma OAI.CubicTorus.radialDensityWeight_tendsto line 435
  40. lemma OAI.CubicTorus.radialDensityMass_tendsto line 452
  41. lemma OAI.CubicTorus.weakCMC_radialDensityMass_monotone line 474
  42. theorem OAI.CubicTorus.weakCMC_cellBallMass_monotone line 489
  43. lemma OAI.CubicTorus.quotientMap_injective_open_closed_cell line 515
  44. lemma OAI.CubicTorus.quotientMap_image_ball line 530
  45. lemma OAI.CubicTorus.compactCell_mem_quotient_ball_iff line 543
  46. lemma OAI.CubicTorus.cellBallMass_eq_spatialNormalMeasure line 556
  47. theorem OAI.CubicTorus.weakCMC_spatial_ball_monotone line 566
  48. lemma OAI.CubicTorus.exists_density_of_cmc_monotone line 592
  49. theorem OAI.CubicTorus.weakCMC_exists_spatial_density line 621
  50. lemma OAI.CubicTorus.isMinimizerAt_density_pos line 633
  51. theorem OAI.CubicTorus.exists_positive_wallVariation_smallShift line 659
  52. def OAI.CubicTorus.quarterCenter line 715
  53. lemma OAI.CubicTorus.smallShift_coordinates line 717
  54. lemma OAI.CubicTorus.smallShift_double_quotient line 729
  55. lemma OAI.CubicTorus.smallShift_center_ball line 743
  56. theorem OAI.CubicTorus.isMinimizerAt_exists_centered_weakCMC line 758
  57. def OAI.CubicTorus.halfspaceIndicator line 801
  58. lemma OAI.CubicTorus.measurable_halfspaceIndicator line 804
  59. lemma OAI.CubicTorus.halfspaceIndicator_bound line 807
  60. lemma OAI.CubicTorus.hyperplane_volume_zero line 811
  61. lemma OAI.CubicTorus.HalfspaceTrappedAt.eventually_characteristic line 820
  62. theorem OAI.CubicTorus.HalfspaceTrappedAt.tendsto_integral_deviation line 856
  63. theorem OAI.CubicTorus.isMinimizerAt_halfspace_blowup_ae line 893