OAI/Geometry/CubicTorus/Compactness/BVLocalTranslation.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.norm_quotientMap_le line 16
  2. def OAI.CubicTorus.shortestLift line 23
  3. lemma OAI.CubicTorus.measurable_shortestLift line 25
  4. lemma OAI.CubicTorus.quotientMap_shortestLift line 28
  5. lemma OAI.CubicTorus.norm_shortestLift line 31
  6. lemma OAI.CubicTorus.abs_flux_local_bound line 35
  7. lemma OAI.CubicTorus.smoothApprox_zero_outside_ball line 65
  8. theorem OAI.CubicTorus.smooth_test_translation_bound_local line 91
  9. theorem OAI.CubicTorus.measurable_test_translation_bound_local line 166
  10. lemma OAI.CubicTorus.torus_test_translation_bound_local line 205
  11. theorem OAI.CubicTorus.characteristic_translation_bound_local line 221
  12. instance OAI.CubicTorus.torus_compactSpace line 266
  13. instance OAI.CubicTorus.torusVolume_negInvariant line 269
  14. theorem OAI.CubicTorus.local_volume_product_le_perimeter line 272
  15. theorem OAI.CubicTorus.isMinimizerAt_perimeter_lower_density line 381
  16. def OAI.CubicTorus.reverseNormal line 418
  17. lemma OAI.CubicTorus.continuous_reverseNormal line 421
  18. lemma OAI.CubicTorus.isNormalMeasure_compl line 424
  19. lemma OAI.CubicTorus.spatialNormalMeasure_reverse line 445
  20. lemma OAI.CubicTorus.perimeter_eq_zero_of_volume_eq_zero line 452
  21. lemma OAI.CubicTorus.spatialNormalMeasure_support_subset_volumeSupport line 456
  22. lemma OAI.CubicTorus.spatialNormalMeasure_support_subset_boundary line 485
  23. theorem OAI.CubicTorus.isMinimizerAt_perimeter_support line 494
  24. def OAI.CubicTorus.supportedMeasure line 524
  25. instance OAI.CubicTorus.supportedMeasure_finite line 527
  26. lemma OAI.CubicTorus.map_supportedMeasure line 530
  27. lemma OAI.CubicTorus.supportedMeasure_closedBall line 535
  28. lemma OAI.CubicTorus.setIntegral_supportedMeasure_closedBall line 544
  29. lemma OAI.CubicTorus.setAverage_supportedMeasure_closedBall line 554
  30. theorem OAI.CubicTorus.isMinimizerAt_supportedMeasure_doubling line 561
  31. theorem OAI.CubicTorus.isMinimizerAt_normal_differentiation line 594
  32. lemma OAI.CubicTorus.normalMeasure_polar_unit line 638
  33. def OAI.CubicTorus.normalExcess line 652
  34. theorem OAI.CubicTorus.isMinimizerAt_normal_excess_ae line 656
  35. theorem OAI.CubicTorus.isMinimizerAt_exists_unit_normal_excess line 717
  36. def OAI.CubicTorus.directionalMass line 740
  37. lemma OAI.CubicTorus.directionalMass_nonneg line 744
  38. lemma OAI.CubicTorus.directionalMass_integrable line 748
  39. lemma OAI.CubicTorus.abs_flux_directional_bound line 755
  40. theorem OAI.CubicTorus.smooth_test_directional_translation_bound line 792
  41. theorem OAI.CubicTorus.measurable_test_directional_translation_bound line 865
  42. lemma OAI.CubicTorus.torus_test_directional_translation_bound line 906
  43. theorem OAI.CubicTorus.characteristic_directional_translation_bound line 924