OAI/Geometry/CubicTorus/Regularity/BVTangentialBlowup.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.normalized_setIntegral_le_average line 16
  2. def OAI.CubicTorus.normalOscillation line 29
  3. lemma OAI.CubicTorus.normalOscillation_nonneg line 33
  4. theorem OAI.CubicTorus.isMinimizerAt_normal_oscillation_ae line 37
  5. lemma OAI.CubicTorus.integrable_norm_sub_normal line 65
  6. lemma OAI.CubicTorus.directionalMass_le_normal_oscillation_integral line 73
  7. lemma OAI.CubicTorus.characteristic_tangential_translation_bound line 87
  8. theorem OAI.CubicTorus.isMinimizerAt_tangential_blowup_ae line 121
  9. lemma OAI.CubicTorus.smoothApprox_nonneg line 163
  10. lemma OAI.CubicTorus.flux_ordered_lower_bound line 168
  11. theorem OAI.CubicTorus.smooth_test_ordered_translation_lower_bound line 213
  12. theorem OAI.CubicTorus.measurable_test_ordered_translation_lower_bound line 285
  13. lemma OAI.CubicTorus.torus_test_ordered_translation_lower_bound line 326
  14. def OAI.CubicTorus.orderDefect line 344
  15. lemma OAI.CubicTorus.orderDefect_nonneg line 347
  16. lemma OAI.CubicTorus.orderDefect_bound line 351
  17. lemma OAI.CubicTorus.measurable_orderDefect line 355
  18. theorem OAI.CubicTorus.characteristic_ordered_translation_bound line 360
  19. theorem OAI.CubicTorus.ordered_volume_product_bound line 402
  20. lemma OAI.CubicTorus.shortestLift_quotientMap line 539
  21. lemma OAI.CubicTorus.shortestLift_eq_of_lift line 545
  22. lemma OAI.CubicTorus.shortestLift_sub_local line 548
  23. lemma OAI.CubicTorus.dist_shortestLift_sub_local line 555
  24. theorem OAI.CubicTorus.isometryOn_shortestLift_chart line 559
  25. lemma OAI.CubicTorus.continuousOn_shortestLift_chart line 568
  26. lemma OAI.CubicTorus.inner_shortestLift_sub_nonneg line 572
  27. lemma OAI.CubicTorus.ordered_density_normal_oscillation line 609
  28. def OAI.CubicTorus.BoundaryFlatAt line 655
  29. lemma OAI.CubicTorus.normal_oscillation_implies_boundary_flatness line 659
  30. theorem OAI.CubicTorus.isMinimizerAt_boundary_flat_ae line 714
  31. def OAI.CubicTorus.normalCap line 743
  32. lemma OAI.CubicTorus.normalCap_eq_image line 746
  33. lemma OAI.CubicTorus.isPreconnected_normalCap line 763
  34. lemma OAI.CubicTorus.preconnected_avoids_frontier line 771
  35. lemma OAI.CubicTorus.normalCap_avoids_frontier line 783
  36. lemma OAI.CubicTorus.normalCap_ball_subset line 791
  37. lemma OAI.CubicTorus.small_oscillation_outward_cap line 815
  38. theorem OAI.CubicTorus.isMinimizerAt_outward_cap_ae line 863
  39. lemma OAI.CubicTorus.polar_reverse_normal line 899
  40. def OAI.CubicTorus.HalfspaceTrappedAt line 914
  41. theorem OAI.CubicTorus.isMinimizerAt_halfspace_trapped_ae line 919