OAI/Geometry/CubicTorus/Regularity/SurfaceGraphBundleMeasure.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.mem_coordinateHalf_quotient line 14
  2. lemma OAI.CubicTorus.coordinateHalf_zero line 28
  3. lemma OAI.CubicTorus.coordinateHalf_one_half line 32
  4. lemma OAI.CubicTorus.coordinateHalf_translation line 38
  5. lemma OAI.CubicTorus.volume_translated_half line 44
  6. theorem OAI.CubicTorus.isMinimizerAt_exists_bisecting_reflection_measurable line 53
  7. theorem OAI.CubicTorus.isMinimizerAt_exists_bisecting_reflection line 88
  8. lemma OAI.CubicTorus.coordinateHalf_open line 117
  9. lemma OAI.CubicTorus.coordinateHalf_eq_slab_image line 123
  10. lemma OAI.CubicTorus.coordinateHalf_preconnected line 146
  11. lemma OAI.CubicTorus.coordinateReflection_preimage_half line 152
  12. lemma OAI.CubicTorus.coordinateHalf_realVolume line 161
  13. lemma OAI.CubicTorus.reflectionCompetitor_retained line 174
  14. lemma OAI.CubicTorus.reflectionCompetitor_invariant line 185
  15. theorem OAI.CubicTorus.cutoff_graph_patch_continuous_mass line 203
  16. theorem OAI.CubicTorus.cutoff_graph_patch_measure line 237
  17. lemma OAI.CubicTorus.graphUnitNormalExtension_measurable line 300
  18. def OAI.CubicTorus.graphNormalSection line 307
  19. lemma OAI.CubicTorus.graphNormalSection_measurable line 311
  20. lemma OAI.CubicTorus.weighted_bundle_section line 315
  21. theorem OAI.CubicTorus.cutoff_graph_patch_bundle_measure line 330
  22. def OAI.CubicTorus.clampCell line 375
  23. lemma OAI.CubicTorus.continuous_clampCell line 380
  24. lemma OAI.CubicTorus.clampCell_coe line 385
  25. def OAI.CubicTorus.normalCellProjection line 392
  26. lemma OAI.CubicTorus.continuous_normalCellProjection line 395
  27. lemma OAI.CubicTorus.normalCellProjection_cover line 398
  28. lemma OAI.CubicTorus.map_withDensity_comp line 403
  29. lemma OAI.CubicTorus.withDensity_restrict_of_support line 413
  30. def OAI.CubicTorus.actualNormalGraphChart line 424
  31. lemma OAI.CubicTorus.actualNormalGraphChart_measurable line 428
  32. theorem OAI.CubicTorus.normalMeasure_graph_area_measure line 434
  33. def OAI.CubicTorus.lpPullbackLE line 491
  34. lemma OAI.CubicTorus.lpPullbackLE_ae line 499
  35. lemma OAI.CubicTorus.lpPullbackLE_congr_ae line 509
  36. lemma OAI.CubicTorus.graphAreaVector_norm_ge_one line 517
  37. lemma OAI.CubicTorus.graph_chart_measure_le line 522
  38. def OAI.CubicTorus.graphCovector line 547
  39. lemma OAI.CubicTorus.graphCovector_apply line 550
  40. lemma OAI.CubicTorus.measurable_graphCovector line 553
  41. lemma OAI.CubicTorus.graphCovector_norm_le line 559
  42. lemma OAI.CubicTorus.graphCovector_memLp line 570
  43. def OAI.CubicTorus.graphCovectorLp line 576
  44. lemma OAI.CubicTorus.graphCovectorLp_ae line 582
  45. lemma OAI.CubicTorus.graphCovector_duality line 604
  46. lemma OAI.CubicTorus.graphCovector_normal_zero line 620
  47. lemma OAI.CubicTorus.gradient_graph_trace line 628
  48. lemma OAI.CubicTorus.actualNormalGraphChart_position line 644
  49. lemma OAI.CubicTorus.actualNormalGraphChart_normal line 653
  50. lemma OAI.CubicTorus.smoothScalarGradient_graph_covector line 658
  51. def OAI.CubicTorus.PlaneWeakGradientOn line 671
  52. lemma OAI.CubicTorus.PlaneWeakGradientOn.congr line 675
  53. lemma OAI.CubicTorus.C1_weak_gradient_on line 687
  54. lemma OAI.CubicTorus.L2_pair_scalar_measure line 716
  55. lemma OAI.CubicTorus.L2_pair_vector_measure line 724
  56. lemma OAI.CubicTorus.PlaneWeakGradientOn.L2_limit line 732
  57. lemma OAI.CubicTorus.graph_trace_contDiffOn_C1 line 766
  58. lemma OAI.CubicTorus.surfaceSmoothJet_chart_weak_gradient line 774
  59. theorem OAI.CubicTorus.surfaceH1_chart_weak_gradient line 815