OAI/Geometry/CubicTorus/Regularity/BVOrientedGraphCost.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.norm_sub_inner_normalized_le line 15
  2. def OAI.CubicTorus.graphSlopeNormal line 28
  3. lemma OAI.CubicTorus.graphSlopeVector_norm_sq line 31
  4. lemma OAI.CubicTorus.graphSlopeVector_norm_ge line 36
  5. lemma OAI.CubicTorus.graphSlopeNormal_unit line 41
  6. def OAI.CubicTorus.graphOrientedCost line 46
  7. lemma OAI.CubicTorus.graphOrientedCost_nonneg line 49
  8. lemma OAI.CubicTorus.graphOrientedCost_continuous line 54
  9. lemma OAI.CubicTorus.graphOrientedCost_slope_le line 58
  10. lemma OAI.CubicTorus.graphOrientedCost_trace_integrable line 72
  11. lemma OAI.CubicTorus.integral_graphSublevel_relative_flux_le line 80
  12. lemma OAI.CubicTorus.normal_constant_admissible line 113
  13. lemma OAI.CubicTorus.cutoff_constant_flux_sub_le line 117
  14. lemma OAI.CubicTorus.cutoff_constant_flux_normal line 156
  15. lemma OAI.CubicTorus.normalMeasure_sublevelCutoff_inner_tendsto line 168
  16. def OAI.CubicTorus.graphBallOrientedCost line 211
  17. lemma OAI.CubicTorus.graphBallOrientedCost_tendsto line 214
  18. def OAI.CubicTorus.bundleOrientedExcess line 268
  19. lemma OAI.CubicTorus.bundleOrientedExcess_eq line 271
  20. theorem OAI.CubicTorus.isMinimizerAt_oriented_graph_replacement line 279
  21. lemma OAI.CubicTorus.planeGradient_contDiff line 365
  22. lemma OAI.CubicTorus.smooth_graph_relative_energy_integrable line 370
  23. lemma OAI.CubicTorus.graphBallOrientedCost_le_disk line 377
  24. lemma OAI.CubicTorus.bundleOrientedExcess_nonneg line 400
  25. lemma OAI.CubicTorus.bundleOrientedExcess_mono line 407
  26. lemma OAI.CubicTorus.compact_convolution_gradient_lipschitz line 433
  27. theorem OAI.CubicTorus.plane_weak_harmonic_smooth_representative line 450
  28. lemma OAI.CubicTorus.plane_gradient_oscillation_energy line 508
  29. theorem OAI.CubicTorus.planar_H1_strong_harmonic_approximation line 532
  30. lemma OAI.CubicTorus.sublevelVolume_relative_difference line 607
  31. lemma OAI.CubicTorus.hasDerivAt_sublevelVolume_of_interior_change line 642
  32. theorem OAI.CubicTorus.isMinimizerAt_oriented_interior_low_slice line 667
  33. def OAI.CubicTorus.graphBlend line 739
  34. lemma OAI.CubicTorus.graphBlend_contDiff line 742
  35. lemma OAI.CubicTorus.graphBlend_eq_of_zero line 747
  36. lemma OAI.CubicTorus.graphBlend_eq_of_one line 750
  37. lemma OAI.CubicTorus.graphBlend_abs_le line 753
  38. lemma OAI.CubicTorus.graphBlend_fderiv line 766
  39. lemma OAI.CubicTorus.norm_add_three_sq_le line 779
  40. lemma OAI.CubicTorus.graphBlend_relative_energy_pointwise line 785
  41. lemma OAI.CubicTorus.graphBlend_relative_energy_cutoff line 805