OAI/Geometry/CubicTorus/Regularity/BVC1Patch.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.MovingCenter.isMinimizerAt_moving_lipschitz_graph line 15
  2. lemma OAI.CubicTorus.polar_tilt_oscillation_scale line 141
  3. lemma OAI.CubicTorus.normalPlaneProjection_eq_embedding line 174
  4. lemma OAI.CubicTorus.normalPlaneProjection_add line 180
  5. lemma OAI.CubicTorus.exact_graph_of_trapped_height line 185
  6. lemma OAI.CubicTorus.normalGraph_hasFDerivWithinAt_of_flat line 255
  7. lemma OAI.CubicTorus.normalGraph_contDiffOn_one_of_continuous_normal line 276
  8. theorem OAI.CubicTorus.MovingCenter.isMinimizerAt_moving_C1_graph line 312
  9. def OAI.CubicTorus.BoundaryC1Patch line 432
  10. def OAI.CubicTorus.C1RegularPoint line 439
  11. lemma OAI.CubicTorus.isOpen_c1RegularPoint line 442
  12. lemma OAI.CubicTorus.c1Patch_of_exact_graph line 448
  13. lemma OAI.CubicTorus.exists_radius_of_normalExcess_tendsto line 480
  14. theorem OAI.CubicTorus.MovingCenter.isMinimizerAt_c1_regular_ae_local line 517
  15. lemma OAI.CubicTorus.support_inter_open_subset_closure line 562
  16. theorem OAI.CubicTorus.MovingCenter.isMinimizerAt_c1_regular_dense_local line 578
  17. theorem OAI.CubicTorus.MovingCenter.isMinimizerAt_c1_singular_null_local line 591
  18. lemma OAI.CubicTorus.isCompact_c1SingularPart line 603
  19. lemma OAI.CubicTorus.smoothApprox_sub_eq_integral line 620
  20. theorem OAI.CubicTorus.smoothApprox_error_local line 633
  21. lemma OAI.CubicTorus.integrable_bounded_one line 695
  22. def OAI.CubicTorus.boundedFunctionL1 line 700
  23. lemma OAI.CubicTorus.boundedFunctionL1_dist line 704
  24. lemma OAI.CubicTorus.totallyBounded_local_smoothApprox line 717
  25. theorem OAI.CubicTorus.totallyBounded_local_translation line 775
  26. lemma OAI.CubicTorus.integral_ball_affine_scaling line 819
  27. lemma OAI.CubicTorus.fundamentalCube_inter_ball_preimage line 840
  28. lemma OAI.CubicTorus.integral_quotient_ball line 856
  29. def OAI.CubicTorus.blowupCharacteristic line 864
  30. lemma OAI.CubicTorus.measurable_blowupCharacteristic line 867
  31. lemma OAI.CubicTorus.blowupCharacteristic_bound line 872
  32. lemma OAI.CubicTorus.blowupCharacteristic_translation_bound line 875