OAI/Geometry/CubicTorus/Compactness/GraphMollifier.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.isMinimizerAt_primary_cone_C1_offvertex line 13
  2. def OAI.CubicTorus.graphMollifier line 57
  3. lemma OAI.CubicTorus.graphMollifier_radius_tendsto line 65
  4. lemma OAI.CubicTorus.graphSmooth_tendsto line 70
  5. theorem OAI.CubicTorus.graphSmooth_fderiv_tendsto line 77
  6. lemma OAI.CubicTorus.graphSmooth_gradient_tendsto line 102
  7. lemma OAI.CubicTorus.graph_trace_volume_zero line 120
  8. lemma OAI.CubicTorus.measurable_graphSublevelIndicator line 135
  9. lemma OAI.CubicTorus.graphSublevelIndicator_bound line 140
  10. lemma OAI.CubicTorus.graphSublevelIndicator_tendsto line 146
  11. lemma OAI.CubicTorus.graphSublevel_flux_mollification_tendsto line 166
  12. lemma OAI.CubicTorus.graphAreaVector_norm_linear line 197
  13. lemma OAI.CubicTorus.graph_trace_zero_outside line 205
  14. theorem OAI.CubicTorus.integral_C1graphSublevel_divergence line 216
  15. lemma OAI.CubicTorus.graphAreaVector_continuousAt line 272
  16. lemma OAI.CubicTorus.graph_weighted_continuous line 277
  17. lemma OAI.CubicTorus.graph_weighted_integrable line 291
  18. lemma OAI.CubicTorus.setIntegral_graphSublevel_divergence line 300
  19. theorem OAI.CubicTorus.blowup_graph_patch_weighted_flux line 318
  20. lemma OAI.CubicTorus.graphSlopeNormal_contDiff line 371
  21. def OAI.CubicTorus.graphUnitNormalExtension line 382
  22. lemma OAI.CubicTorus.graphUnitNormalExtension_unit line 385
  23. lemma OAI.CubicTorus.graphUnitNormalExtension_contDiff line 389
  24. lemma OAI.CubicTorus.graphUnitNormalExtension_graph line 398
  25. lemma OAI.CubicTorus.graphUnitNormalExtension_tendsto line 405
  26. lemma OAI.CubicTorus.graphAreaVector_inner_unit line 412
  27. lemma OAI.CubicTorus.graph_area_trace_mollified_normal_tendsto line 431
  28. theorem OAI.CubicTorus.blowup_graph_patch_weighted_mass line 465
  29. lemma OAI.CubicTorus.normalPlaneCoordinates_norm_le line 531
  30. lemma OAI.CubicTorus.graph_weighted_normal_tendsto line 535
  31. theorem OAI.CubicTorus.blowup_graph_patch_normal_ae line 551
  32. theorem OAI.CubicTorus.blowup_graph_patch_signed_mass line 629
  33. lemma OAI.CubicTorus.weighted_tendsto_on_tsupport line 690
  34. theorem OAI.CubicTorus.blowup_graph_patch_limit_mass line 699
  35. lemma OAI.CubicTorus.contDiff_divergence line 766
  36. lemma OAI.CubicTorus.contDiff_tangentialDivergence_normal line 774
  37. lemma OAI.CubicTorus.continuous_tangentialDivergence_normal line 779
  38. theorem OAI.CubicTorus.blowup_C1graph_stationary line 783