OAI/Geometry/CubicTorus/Regularity/BVBlowupNormalMeasure.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.CubicTorus.finiteMeasure_cover_closedBall line 15
  2. lemma OAI.CubicTorus.blowupCharacteristic_translation_density line 19
  3. theorem OAI.CubicTorus.totallyBounded_blowupCharacteristic line 45
  4. abbrev OAI.CubicTorus.BlowupNormalBundle line 89
  5. def OAI.CubicTorus.blowupNormalMap line 91
  6. lemma OAI.CubicTorus.continuous_blowupNormalMap line 94
  7. def OAI.CubicTorus.blowupNormalMeasure line 100
  8. lemma OAI.CubicTorus.blowupNormalMeasure_mass line 105
  9. lemma OAI.CubicTorus.blowupNormalMap_mem line 117
  10. lemma OAI.CubicTorus.blowupNormalMeasure_supported line 126
  11. theorem OAI.CubicTorus.blowupNormalMeasure_cluster line 142
  12. lemma OAI.CubicTorus.integral_blowupNormalMeasure line 177
  13. lemma OAI.CubicTorus.tangentialDivergence_zero_of_notMem_tsupport line 189
  14. lemma OAI.CubicTorus.hasCompactSupport_normalBundle_test line 193
  15. lemma OAI.CubicTorus.continuous_blowupFluxTest line 204
  16. lemma OAI.CubicTorus.continuous_blowupTangentTest line 208
  17. def OAI.CubicTorus.blowupFluxTest line 216
  18. def OAI.CubicTorus.blowupTangentTest line 222
  19. lemma OAI.CubicTorus.integral_blowup_test line 228
  20. lemma OAI.CubicTorus.tangentialDivergence_scaledTestField line 239
  21. theorem OAI.CubicTorus.weakCMC_blowup_identity line 246
  22. theorem OAI.CubicTorus.weakCMC_blowup_limit_stationary line 274
  23. lemma OAI.CubicTorus.cover_indicator_bound line 306
  24. lemma OAI.CubicTorus.boundedFunctionL1_ae line 311
  25. theorem OAI.CubicTorus.exists_cover_indicator_limit line 315
  26. lemma OAI.CubicTorus.boundedFunctionL1_integral_tendsto line 358
  27. theorem OAI.CubicTorus.isMinimizerAt_blowup_limit line 379
  28. lemma OAI.CubicTorus.integral_blowupCharacteristic_ball line 433
  29. lemma OAI.CubicTorus.localL1_integral_tendsto line 443
  30. lemma OAI.CubicTorus.localL1_ball_integral_tendsto line 466
  31. theorem OAI.CubicTorus.isMinimizerAt_blowup_limit_density line 478
  32. lemma OAI.CubicTorus.localL1_weighted_integral_tendsto line 571
  33. theorem OAI.CubicTorus.blowup_limit_flux line 602
  34. def OAI.CubicTorus.coverLocalPerimeter line 662
  35. lemma OAI.CubicTorus.coverLocalPerimeter_mono line 667
  36. lemma OAI.CubicTorus.integral_divergence_le_coverLocalPerimeter line 682
  37. theorem OAI.CubicTorus.coverLocalPerimeter_le_normal line 693
  38. def OAI.CubicTorus.coverPrismCoordinates line 745
  39. lemma OAI.CubicTorus.coverPrismCoordinates_apply line 757
  40. lemma OAI.CubicTorus.coverPrismCoordinates_symm_apply line 760
  41. lemma OAI.CubicTorus.coverPrismCoordinates_measurePreserving line 763
  42. lemma OAI.CubicTorus.coverPrismCoordinates_symm_measurePreserving line 774
  43. lemma OAI.CubicTorus.prism_component_contDiff line 778
  44. lemma OAI.CubicTorus.prism_component_compactSupport line 783
  45. lemma OAI.CubicTorus.prism_component_fderiv line 796
  46. lemma OAI.CubicTorus.prism_coordinate_divergence line 803
  47. def OAI.CubicTorus.euclideanPrism line 819
  48. lemma OAI.CubicTorus.measurableSet_euclideanPrism line 822
  49. theorem OAI.CubicTorus.integral_euclideanPrism_divergence line 826