OAI/Geometry/IntegralFillings/Optimality/BallBoundary.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpIntegralFillings.Optimality.integral_boundary line 15
  2. lemma OAI.SharpIntegralFillings.Optimality.boundary_isCycle line 27
  3. lemma OAI.SharpIntegralFillings.Optimality.push_compactlySupported line 34
  4. def OAI.SharpIntegralFillings.Optimality.clippedCoord line 47
  5. lemma OAI.SharpIntegralFillings.Optimality.clippedCoord_lipschitz line 50
  6. lemma OAI.SharpIntegralFillings.Optimality.clippedCoord_abs_le line 53
  7. lemma OAI.SharpIntegralFillings.Optimality.clippedCoord_boundedLip line 57
  8. lemma OAI.SharpIntegralFillings.Optimality.clippedCoord_on_unitBall line 60
  9. def OAI.SharpIntegralFillings.Optimality.ambientBall line 66
  10. lemma OAI.SharpIntegralFillings.Optimality.inclusion_lipschitz line 69
  11. lemma OAI.SharpIntegralFillings.Optimality.ambientBall_integral line 72
  12. lemma OAI.SharpIntegralFillings.Optimality.ambientBall_metric line 76
  13. lemma OAI.SharpIntegralFillings.Optimality.ambientBall_boundary_mass_le line 79
  14. lemma OAI.SharpIntegralFillings.Optimality.ambientBall_boundary_compact line 87
  15. lemma OAI.SharpIntegralFillings.Optimality.ambientBall_boundary_coords line 93
  16. lemma OAI.SharpIntegralFillings.Optimality.allFillings_mass_ge_ball line 109
  17. lemma OAI.SharpIntegralFillings.Optimality.ambientBall_boundary_mass_pos line 127