OAI/Geometry/CubicTorus/Profiles/Endpoint.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.plane_symmetric_unit_kernel line 15
  2. lemma OAI.CubicTorus.normal_unit_kernel_shape line 76
  3. lemma OAI.CubicTorus.normal_unit_kernel_trace_square line 124
  4. theorem OAI.CubicTorus.measure_eq_of_smooth_bounded_integrals line 175
  5. theorem OAI.CubicTorus.cutoff_graph_patch_measure_eq line 215
  6. lemma OAI.CubicTorus.measurable_graphUnitNormalExtension line 283
  7. theorem OAI.CubicTorus.cutoff_graph_patch_normal_measure_eq line 290
  8. lemma OAI.CubicTorus.sibling_map_withDensity_comp line 358
  9. lemma OAI.CubicTorus.projected_cutoff_measure line 367
  10. lemma OAI.CubicTorus.normalCoverMeasure_reverse_projected line 377
  11. theorem OAI.CubicTorus.normalMeasure_graph_patch_measure_eq line 387
  12. theorem OAI.CubicTorus.centered_graph_phase_patch_of_boundary line 439
  13. theorem OAI.CubicTorus.actual_centered_compact_normal_chart line 499
  14. theorem OAI.CubicTorus.actual_centered_small_slope_normal_chart line 549
  15. theorem OAI.CubicTorus.actual_centered_compact_small_normal_chart line 686
  16. lemma OAI.CubicTorus.normalGraph_map_volume_le_of_lower_density line 739
  17. theorem OAI.CubicTorus.isMinimizerAt_dominated_normal_chart line 771