OAI/Geometry/CubicTorus/Regularity/NormalCoverMap.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicTorus.normalCoverMap line 13
  2. lemma OAI.CubicTorus.continuous_normalCoverMap line 15
  3. def OAI.CubicTorus.normalCoverMeasure line 18
  4. lemma OAI.CubicTorus.normalCoverMeasure_integral line 21
  5. def OAI.CubicTorus.HasCutoffSaturation line 28
  6. lemma OAI.CubicTorus.normalMeasure_cutoff_saturation line 37
  7. lemma OAI.CubicTorus.normalCoverMeasure_local_flux line 62
  8. lemma OAI.CubicTorus.normalCoverMeasure_CMC line 76
  9. theorem OAI.CubicTorus.cutoff_graph_patch_weighted_mass line 98
  10. theorem OAI.CubicTorus.cutoff_graph_patch_normal_ae line 163
  11. theorem OAI.CubicTorus.cutoff_graph_patch_signed_mass line 241
  12. theorem OAI.CubicTorus.cutoff_graph_patch_limit_mass line 302
  13. theorem OAI.CubicTorus.cutoff_C1graph_firstVariation line 369
  14. theorem OAI.CubicTorus.isMinimizerAt_strict_C1_cone_blowup line 462
  15. lemma OAI.CubicTorus.coverEssentialBoundary_eq_support line 542
  16. lemma OAI.CubicTorus.coverEssentialBoundary_compl line 559
  17. lemma OAI.CubicTorus.cover_boundary_local_ae line 563
  18. lemma OAI.CubicTorus.cover_boundary_preimage_image line 570
  19. lemma OAI.CubicTorus.cover_boundary_measurePreserving_homeomorph line 576
  20. theorem OAI.CubicTorus.connected_cover_phase line 589
  21. lemma OAI.CubicTorus.cover_halfballs_null line 633
  22. lemma OAI.CubicTorus.cover_opposite_halfballs_model line 646
  23. theorem OAI.CubicTorus.cover_boundary_plane_phases line 665
  24. theorem OAI.CubicTorus.cover_flattened_boundary_phases line 714
  25. def OAI.CubicTorus.graphSignedHeight line 757
  26. lemma OAI.CubicTorus.graphSignedHeight_shear line 760
  27. lemma OAI.CubicTorus.graphSignedHeight_graph line 769
  28. theorem OAI.CubicTorus.cover_graph_boundary_phases line 776
  29. def OAI.CubicTorus.dilatedGraph line 821
  30. lemma OAI.CubicTorus.normalGraph_dilated line 823
  31. lemma OAI.CubicTorus.dilatedGraph_lipschitz line 830
  32. lemma OAI.CubicTorus.dilatedGraph_contDiffAt line 836