OAI/Geometry/CubicTorus/Regularity/BVPlaneAreaCoordinates.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.normalPlaneEmbedding_coordinates_of_inner_zero line 15
  2. lemma OAI.CubicTorus.normalPlaneCoordinates_norm_of_inner_zero line 25
  3. theorem OAI.CubicTorus.integral_normalPlane_eq_isometry line 29
  4. lemma OAI.CubicTorus.radial_face_coefficients line 43
  5. def OAI.CubicTorus.radialFaceNormal line 51
  6. lemma OAI.CubicTorus.radialFaceNormal_norm line 54
  7. def OAI.CubicTorus.radialFaceIsometry line 60
  8. lemma OAI.CubicTorus.radialFaceIsometry_perp line 72
  9. theorem OAI.CubicTorus.integral_radialFace line 78
  10. def OAI.CubicTorus.strictPatchOpen line 98
  11. def OAI.CubicTorus.strictPatchClosed line 99
  12. def OAI.CubicTorus.strictPatchCutoff line 100
  13. lemma OAI.CubicTorus.strictPatchCutoff_contDiff line 103
  14. lemma OAI.CubicTorus.strictPatchCutoff_bounds line 109
  15. lemma OAI.CubicTorus.strictPatchCutoff_support line 116
  16. lemma OAI.CubicTorus.strictPatchCutoff_tsupport_open line 133
  17. lemma OAI.CubicTorus.strictPatchOpen_subset_closed line 139
  18. lemma OAI.CubicTorus.strictPatchCutoff_hasCompactSupport line 142
  19. lemma OAI.CubicTorus.measurableSet_strictPatchOpen line 148
  20. lemma OAI.CubicTorus.strictPatchCutoff_tendsto line 154
  21. lemma OAI.CubicTorus.blowup_weighted_remainder_le line 193
  22. theorem OAI.CubicTorus.blowup_two_flat_patches_remainder_le line 219
  23. theorem OAI.CubicTorus.strictPatchCutoff_integral_tendsto line 289
  24. lemma OAI.CubicTorus.strictPatchCutoff_disjoint_sum_le_one line 325
  25. theorem OAI.CubicTorus.blowup_two_polytope_patches_remainder_le line 353
  26. lemma OAI.CubicTorus.abs_prismRadialFlux_le line 421
  27. lemma OAI.CubicTorus.cover_field_planar_sq_bound line 449
  28. lemma OAI.CubicTorus.cover_field_component_bound line 454
  29. theorem OAI.CubicTorus.coverLocalPerimeter_euclideanPrism_le line 458
  30. theorem OAI.CubicTorus.euclideanPrism_closing_error_bound line 478
  31. theorem OAI.CubicTorus.integral_prism_surgery line 502
  32. theorem OAI.CubicTorus.integral_prism_surgery_error line 523
  33. theorem OAI.CubicTorus.coverLocalPerimeter_prism_surgery_le line 539
  34. lemma OAI.CubicTorus.prism_surgery_symmDiff_subset line 560
  35. def OAI.CubicTorus.radialPatchInequalities line 580
  36. lemma OAI.CubicTorus.radialPatchInequalities_contDiff line 584
  37. lemma OAI.CubicTorus.mem_radialPatchOpen line 596
  38. lemma OAI.CubicTorus.mem_radialPatchClosed line 601
  39. lemma OAI.CubicTorus.radialPatchClosed_isCompact line 606
  40. lemma OAI.CubicTorus.radialPatchOpen_disjoint line 633
  41. lemma OAI.CubicTorus.radialFaceIsometry_preimage_patch line 643
  42. def OAI.CubicTorus.planeFaceCoordinates line 678
  43. lemma OAI.CubicTorus.planeFaceCoordinates_measurePreserving line 690
  44. lemma OAI.CubicTorus.radial_face_patch_area line 693
  45. lemma OAI.CubicTorus.integral_plane_coordinate_rectangle line 708
  46. theorem OAI.CubicTorus.radial_face_patch_integral line 734
  47. lemma OAI.CubicTorus.setIntegral_normalPlane_eq_isometry line 767
  48. lemma OAI.CubicTorus.real_volume_normalPlane_eq_isometry line 782
  49. lemma OAI.CubicTorus.inner_radialFaceNormal line 789
  50. theorem OAI.CubicTorus.radial_face_flux line 794
  51. theorem OAI.CubicTorus.neg_radial_face_flux line 811