OAI/Geometry/CubicTorus/Regularity/MinimalGraphDensity.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicTorus.minimalGraphDensity line 13
  2. lemma OAI.CubicTorus.graphAreaVector_norm_sqrt line 16
  3. lemma OAI.CubicTorus.minimalGraphDensity_tsupport line 20
  4. lemma OAI.CubicTorus.minimalGraphDensity_integrable line 27
  5. lemma OAI.CubicTorus.continuous_mul_on_tsupport line 43
  6. lemma OAI.CubicTorus.integrable_mul_on_tsupport line 49
  7. lemma OAI.CubicTorus.planarWedgeChart_continuous line 66
  8. lemma OAI.CubicTorus.slopeScalarTest_support_coordinates line 69
  9. lemma OAI.CubicTorus.planarWedgeChart_coordinates_inverse line 91
  10. lemma OAI.CubicTorus.slopeScalarTest_compactSupport line 97
  11. lemma OAI.CubicTorus.slopeScalarTest_derivative_zero line 106
  12. lemma OAI.CubicTorus.plane_norm_sq_coordinates line 127
  13. lemma OAI.CubicTorus.exists_smooth_radial_test line 132
  14. lemma OAI.CubicTorus.minimalGraphDensity_slope line 144
  15. theorem OAI.CubicTorus.stationary_euler_graph_affine line 156
  16. def OAI.CubicTorus.graphReparam line 260
  17. lemma OAI.CubicTorus.graphReparam_fderiv line 263
  18. lemma OAI.CubicTorus.graphReparam_gradient line 272
  19. lemma OAI.CubicTorus.minimalGraphDensity_reparam line 280
  20. lemma OAI.CubicTorus.integral_minimalGraphDensity_reparam line 290
  21. lemma OAI.CubicTorus.graphReparam_contDiffAt line 300
  22. lemma OAI.CubicTorus.graphReparam_contDiff line 305
  23. lemma OAI.CubicTorus.graphReparam_zero_tsupport line 310
  24. lemma OAI.CubicTorus.positive_wedge_rectangle line 330
  25. theorem OAI.CubicTorus.local_euler_graph_linear line 350
  26. theorem OAI.CubicTorus.local_euler_graph_linear_of_ne_zero line 392
  27. lemma OAI.CubicTorus.normalPlaneEmbedding_inner_coordinates line 457
  28. lemma OAI.CubicTorus.normalGraph_coordinates_eq_iff line 465
  29. def OAI.CubicTorus.rebasedGraph line 473
  30. lemma OAI.CubicTorus.rebasedGraph_apply line 476
  31. lemma OAI.CubicTorus.rebasedGraph_fderiv line 479
  32. lemma OAI.CubicTorus.normalGraph_rebased line 485
  33. lemma OAI.CubicTorus.rebasedGraph_graph_eq line 497
  34. lemma OAI.CubicTorus.rebasedGraph_continuous line 503
  35. lemma OAI.CubicTorus.rebasedGraph_weak_equation line 507
  36. theorem OAI.CubicTorus.conical_stationary_patch_plane line 548
  37. lemma OAI.CubicTorus.coverEssentialBoundary_isClosed line 653
  38. lemma OAI.CubicTorus.inner_kernel_mono_of_local line 657
  39. lemma OAI.CubicTorus.inner_kernel_eq_of_local line 673
  40. lemma OAI.CubicTorus.normal_plane_disk_preconnected line 680
  41. theorem OAI.CubicTorus.local_plane_disk_continuation line 708
  42. lemma OAI.CubicTorus.two_cover_planes_meet line 758
  43. theorem OAI.CubicTorus.closed_locally_planar_single_plane line 786
  44. lemma OAI.CubicTorus.cover_punctured_ball_preconnected line 805
  45. lemma OAI.CubicTorus.cover_boundary_nonzero line 835