OAI/Geometry/RCD/Sobolev/LocalLipschitzAverages.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.local_lipschitz_ball_average_bound line 18

   Source documentation

   Only Lipschitz control on the set containing the two averaging balls is needed; a real-valued Lipschitz extension is used solely for this estimate.

   theorem local_lipschitz_ball_average_bound {S : Set X} {f : X → ℝ} {L : ℝ≥0}
       (hf : LipschitzOnWith L f S) (x y : X) {r : ℝ} (hr : 0 ≤ r)
       (hx : μ (closedBall x r) ≠ 0) (hy : μ (closedBall y r) ≠ 0)
       (hxS : closedBall x r ⊆ S) (hyS : closedBall y r ⊆ S) :
       |(⨍ z in closedBall x r, f z ∂μ)-(⨍ z in closedBall y r, f z ∂μ)| ≤
         L*(dist x y+2*r) := by
   …