OAI/Geometry/CubicTorus/Regularity/CoverEssentialBoundary.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.normalGraph_rescale line 13
  2. lemma OAI.CubicTorus.rescaled_lipschitz_graph line 22
  3. theorem OAI.CubicTorus.actual_boundary_rescaled_graph_packet line 34
  4. def OAI.CubicTorus.coverEssentialBoundary line 155
  5. lemma OAI.CubicTorus.cover_integral_indicator_ball line 159
  6. lemma OAI.CubicTorus.localL1_set_integral_tendsto line 166
  7. lemma OAI.CubicTorus.integral_blowupCharacteristic_ball_center line 176
  8. theorem OAI.CubicTorus.isMinimizerAt_rescaled_boundary_limit line 191
  9. theorem OAI.CubicTorus.isMinimizerAt_rescaled_frontier_approximation line 282
  10. theorem OAI.CubicTorus.normal_graph_C1_subsequence line 361
  11. lemma OAI.CubicTorus.normalGraph_residual_lipschitz line 479
  12. lemma OAI.CubicTorus.normalGraph_norm_le line 491
  13. theorem OAI.CubicTorus.rescaled_actual_graph_limit line 496
  14. theorem OAI.CubicTorus.actual_strong_limit_C1_graph line 606
  15. lemma OAI.CubicTorus.volume_real_affine_preimage_ball_center line 669
  16. lemma OAI.CubicTorus.coverEssentialBoundary_affine line 681
  17. def OAI.CubicTorus.CoverC1BoundaryAt line 701
  18. theorem OAI.CubicTorus.actual_primary_offvertex_fixed_graphs line 722
  19. theorem OAI.CubicTorus.actual_primary_offvertex_C1 line 792