OAI/Geometry/CubicTorus/Regularity/BVBlowupComplement.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.prismRadialFlux_eq_sub line 15
  2. theorem OAI.CubicTorus.blowup_radial_faces_remainder_le line 34
  3. theorem OAI.CubicTorus.coverLocalPerimeter_prism_surgery_lt line 95
  4. theorem OAI.CubicTorus.no_minimizing_strict_prism_sector line 140
  5. lemma OAI.CubicTorus.exists_normal_sphere_null_radius line 181
  6. lemma OAI.CubicTorus.normal_closedBall_ae_eq_ball line 191
  7. theorem OAI.CubicTorus.coverLocalPerimeter_closedBall_eq_ball_of_normal line 200
  8. theorem OAI.CubicTorus.normal_radius_local_minimizing line 217
  9. lemma OAI.CubicTorus.euclideanPrism_mono_height line 249
  10. lemma OAI.CubicTorus.radialPatchOpen_mono_height line 254
  11. theorem OAI.CubicTorus.no_minimizing_small_radial_sector line 261
  12. lemma OAI.CubicTorus.integral_cover_divergence_zero line 303
  13. lemma OAI.CubicTorus.integral_cover_divergence_compl line 330
  14. theorem OAI.CubicTorus.coverLocalPerimeter_compl line 340
  15. def OAI.CubicTorus.reverseBlowupNormal line 375
  16. lemma OAI.CubicTorus.continuous_reverseBlowupNormal line 378
  17. lemma OAI.CubicTorus.reverseBlowupNormal_spatial_mass line 381
  18. lemma OAI.CubicTorus.reverseBlowupNormal_flux line 389
  19. lemma OAI.CubicTorus.coverLocalPerimeter_normal_compl line 405
  20. lemma OAI.CubicTorus.coverLocalPerimeter_compl_minimizing line 412
  21. theorem OAI.CubicTorus.no_minimizing_small_empty_radial_sector line 438
  22. theorem OAI.CubicTorus.no_moving_tangent_small_radial_sector line 463
  23. lemma OAI.CubicTorus.prismSlope_quasiMeasurePreserving line 513
  24. lemma OAI.CubicTorus.mem_negative_radial_halfspace line 523
  25. lemma OAI.CubicTorus.mem_radial_halfspace line 530
  26. theorem OAI.CubicTorus.slope_interval_radial_models line 537
  27. lemma OAI.CubicTorus.cover_norm_le_coordinates line 589
  28. lemma OAI.CubicTorus.radialPatchClosed_coordinate_bounds line 599
  29. lemma OAI.CubicTorus.radialPatchClosed_norm_le line 613
  30. lemma OAI.CubicTorus.euclideanPrism_subset_radialPatchClosed line 620
  31. lemma OAI.CubicTorus.radialPatchOpen_subset_closed line 627
  32. theorem OAI.CubicTorus.exists_small_sector_geometry line 633
  33. lemma OAI.CubicTorus.prismRotatedColumn_measurePreserving line 707
  34. lemma OAI.CubicTorus.prismPlanarProjection_quasiMeasurePreserving line 712
  35. theorem OAI.CubicTorus.prismFrame_product_model line 718
  36. theorem OAI.CubicTorus.prismFrame_angular_sector_model line 729
  37. lemma OAI.CubicTorus.divergence_eq_trace line 758
  38. lemma OAI.CubicTorus.divergence_isometry_pullback line 763
  39. lemma OAI.CubicTorus.isometry_pullback_contDiff line 776
  40. lemma OAI.CubicTorus.isometry_pullback_compactSupport line 781
  41. lemma OAI.CubicTorus.isometry_pullback_tsupport line 785
  42. lemma OAI.CubicTorus.setIntegral_divergence_isometry_preimage line 801
  43. theorem OAI.CubicTorus.coverLocalPerimeter_isometry_preimage line 809