OAI/Geometry/CubicTorus/Estimates/BVPlanarLocalModels.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.planar_cone_rotation line 15
  2. lemma OAI.CubicTorus.planar_directional_bv_rotation line 27
  3. theorem OAI.CubicTorus.planar_cone_finite_angular_transitions_rotated line 57
  4. lemma OAI.CubicTorus.ae_not_phase_of_inter_null line 84
  5. lemma OAI.CubicTorus.ae_phase_of_inter_compl_null line 88
  6. theorem OAI.CubicTorus.angular_finite_local_model line 93
  7. lemma OAI.CubicTorus.triangular_inv_mul_quasiMeasurePreserving line 164
  8. def OAI.CubicTorus.planarWedgeCoordinates line 181
  9. lemma OAI.CubicTorus.planarWedgeCoordinates_quasiMeasurePreserving line 184
  10. lemma OAI.CubicTorus.planarWedgeChart_coordinates line 189
  11. lemma OAI.CubicTorus.planarWedgeCoordinates_chart line 194
  12. theorem OAI.CubicTorus.planar_cone_local_slope_model line 199
  13. lemma OAI.CubicTorus.planeProductCoordinates_apply line 250
  14. lemma OAI.CubicTorus.planeProductCoordinates_symm_apply line 253
  15. def OAI.CubicTorus.coverPlaneCoordinates line 259
  16. lemma OAI.CubicTorus.coverPlaneCoordinates_apply line 262
  17. lemma OAI.CubicTorus.coverPlaneCoordinates_norm_sq line 266
  18. def OAI.CubicTorus.coverPlaneRotationCLE line 273
  19. lemma OAI.CubicTorus.coverPlaneRotationCLE_coordinates line 277
  20. def OAI.CubicTorus.coverPlaneRotation line 282
  21. def OAI.CubicTorus.swapPrismPlane line 291
  22. lemma OAI.CubicTorus.swapPrismPlane_apply line 294
  23. def OAI.CubicTorus.prismFrame line 299
  24. lemma OAI.CubicTorus.normalColumnChart_zero_coordinates line 302
  25. lemma OAI.CubicTorus.prismFrame_apply line 311
  26. lemma OAI.CubicTorus.prismColumnCoordinates_measurePreserving line 319
  27. lemma OAI.CubicTorus.finiteMeasure_real_open_le_of_eventually_le line 340
  28. theorem OAI.CubicTorus.moving_blowup_normal_mass_le_competitor line 369
  29. lemma OAI.CubicTorus.normalMeasure_ball_le_of_smaller line 434
  30. theorem OAI.CubicTorus.moving_blowup_perimeter_eq_normal_ball line 474
  31. lemma OAI.CubicTorus.blowup_test_inner_bound line 523
  32. theorem OAI.CubicTorus.blowupNormal_weighted_saturation line 530
  33. lemma OAI.CubicTorus.setIntegral_divergence_congr_local line 615
  34. lemma OAI.CubicTorus.coverLocalPerimeter_congr_local line 631
  35. def OAI.CubicTorus.coverHalfspace line 655
  36. lemma OAI.CubicTorus.measurableSet_coverHalfspace line 657
  37. lemma OAI.CubicTorus.halfspace_indicator_eq line 660
  38. lemma OAI.CubicTorus.setIntegral_coverHalfspace_divergence line 663
  39. lemma OAI.CubicTorus.coverHalfspace_flux_le line 672
  40. lemma OAI.CubicTorus.coverLocalPerimeter_halfspace_le line 705
  41. theorem OAI.CubicTorus.coverLocalPerimeter_halfspace line 715
  42. lemma OAI.CubicTorus.plane_scalar_trace_integrable line 754
  43. theorem OAI.CubicTorus.blowup_flat_patch_weighted_flux line 765
  44. theorem OAI.CubicTorus.blowup_flat_patch_weighted_mass line 799
  45. theorem OAI.CubicTorus.blowup_flat_patch_normal line 850