OAI/Geometry/CubicTorus/Regularity/BVBlowupRigidCovariance.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicTorus.pullbackBlowupNormal line 15
  2. lemma OAI.CubicTorus.continuous_pullbackBlowupNormal line 18
  3. lemma OAI.CubicTorus.pullbackBlowupNormal_spatial_mass line 23
  4. lemma OAI.CubicTorus.pullbackBlowupNormal_flux line 35
  5. lemma OAI.CubicTorus.coverLocalPerimeter_isometry_normal line 71
  6. lemma OAI.CubicTorus.coverLocalPerimeter_isometry_minimizing line 79
  7. theorem OAI.CubicTorus.no_minimizing_angular_sector line 110
  8. theorem OAI.CubicTorus.no_minimizing_angular_phase_sector line 150
  9. theorem OAI.CubicTorus.no_moving_product_angular_sector line 178
  10. lemma OAI.CubicTorus.slopeScalarTest_tsupport_rectangle_wide line 246
  11. lemma OAI.CubicTorus.slopeScalarTest_hasCompactSupport_wide line 264
  12. theorem OAI.CubicTorus.planar_slope_flux_wide line 271
  13. theorem OAI.CubicTorus.planar_cone_slope_section_wide line 341
  14. theorem OAI.CubicTorus.planar_slope_directional_bound_wide line 409
  15. lemma OAI.CubicTorus.slope_rectangle_ball_wide line 447
  16. theorem OAI.CubicTorus.planar_cone_angular_dual_bv_wide line 469
  17. lemma OAI.CubicTorus.scaled_test_deriv line 539
  18. lemma OAI.CubicTorus.scaled_setIntegral_deriv line 546
  19. lemma OAI.CubicTorus.angular_dual_bv_rescale line 566
  20. lemma OAI.CubicTorus.volume_positive_mul_preimage line 590
  21. lemma OAI.CubicTorus.mul_preimage_phase_ball line 602
  22. lemma OAI.CubicTorus.angularEssentialBoundary_mul_preimage line 609
  23. theorem OAI.CubicTorus.angular_dual_bv_finite_transitions_wide line 630
  24. lemma OAI.CubicTorus.planarWedgeCoordinates_smul line 663
  25. theorem OAI.CubicTorus.planar_cone_annulus_to_vertex line 671
  26. theorem OAI.CubicTorus.planar_cone_wide_vertex_section line 734
  27. lemma OAI.CubicTorus.angularEssentialBoundary_compl line 794
  28. lemma OAI.CubicTorus.nonempty_interval_two_phases_not_null line 800
  29. lemma OAI.CubicTorus.finite_angular_next_transition line 810
  30. theorem OAI.CubicTorus.occupied_adjacent_angular_model line 833
  31. theorem OAI.CubicTorus.adjacent_angular_sector_model line 880