OAI/Geometry/CubicTorus/Regularity/BVPlanarAngularChart.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.euclideanNormalMeasure_ball line 15
  2. lemma OAI.CubicTorus.euclideanNormalMeasure_ball_tendsto line 37
  3. theorem OAI.CubicTorus.euclidean_normal_limit_ball_mass line 54
  4. theorem OAI.CubicTorus.stationary_pair_secondary_cone line 91
  5. lemma OAI.CubicTorus.normalColumnChart_smul line 157
  6. theorem OAI.CubicTorus.conical_product_planar_cone line 166
  7. lemma OAI.CubicTorus.triangular_mul_quasiMeasurePreserving line 221
  8. def OAI.CubicTorus.planarWedgeChart line 242
  9. lemma OAI.CubicTorus.planarWedgeChart_quasiMeasurePreserving line 245
  10. lemma OAI.CubicTorus.planarWedgeChart_smul line 251
  11. lemma OAI.CubicTorus.planar_cone_all_positive_scales line 257
  12. theorem OAI.CubicTorus.planar_cone_slope_section line 273
  13. def OAI.CubicTorus.slopeScalarTest line 353
  14. def OAI.CubicTorus.slopeVerticalVector line 357
  15. lemma OAI.CubicTorus.slopeScalarTest_contDiff line 359
  16. lemma OAI.CubicTorus.slopeScalarTest_vertical_derivative line 377
  17. lemma OAI.CubicTorus.slopeScalarTest_tsupport_rectangle line 404
  18. lemma OAI.CubicTorus.slopeScalarTest_hasCompactSupport line 422
  19. theorem OAI.CubicTorus.planar_slope_flux line 429
  20. def OAI.CubicTorus.planarAxialBump line 511
  21. lemma OAI.CubicTorus.planarAxialBump_support line 517
  22. theorem OAI.CubicTorus.planar_product_directional_bound line 522
  23. lemma OAI.CubicTorus.slopeVerticalVector_norm line 576
  24. lemma OAI.CubicTorus.slopeScalarTest_bound line 581
  25. theorem OAI.CubicTorus.planar_slope_directional_bound line 587
  26. lemma OAI.CubicTorus.slope_rectangle_ball line 625
  27. theorem OAI.CubicTorus.planar_cone_angular_dual_bv line 643
  28. def OAI.CubicTorus.angularEssentialBoundary line 709
  29. lemma OAI.CubicTorus.angular_essential_boundary_in_mixed_closure line 713
  30. theorem OAI.CubicTorus.angular_dual_bv_finite_transitions line 741
  31. theorem OAI.CubicTorus.planar_cone_finite_angular_transitions line 766
  32. lemma OAI.CubicTorus.angularEssentialBoundary_eq_support line 792
  33. theorem OAI.CubicTorus.connected_angular_phase line 801
  34. lemma OAI.CubicTorus.measure_inter_ball_zero_of_sides line 834
  35. theorem OAI.CubicTorus.finite_angular_transition_is_jump line 847