OAI/Geometry/RCD/Sobolev/LocalGradientRepresentative.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.local_average_bound_of_gradient line 18

   Source documentation

   Transport between small balls controls their averages by the weak upper gradient, with no volume-comparison factor.

   theorem NoncollapsedRCD.local_average_bound_of_gradient
       (K : ℝ) (n : ℕ) (hn : 2 ≤ n) (hX : NoncollapsedRCD K n X)
       {u G : Lp ℝ 2 (hausdorff n X)} (hG : IsRelaxedSlope (hausdorff n X) u G)
       (L : ℝ≥0) {p : X} {R : ℝ} (hR : 0 < R)
       (hGb : ∀ᵐ x ∂(hausdorff n X).restrict (ball p (8 * R)), G x ≤ L)
       (x y : X) (hx : x ∈ closedBall p R) (hy : y ∈ closedBall p R)
       (r : ℝ) (hr : 0 < r) (hrR : r ≤ R) :
       |(⨍ z in closedBall x r, u z ∂hausdorff n X)-
         (⨍ z in closedBall y r, u z ∂hausdorff n X)| ≤ L*(dist x y+2*r) := by
   …

   Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.IsRelaxedSlope

2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.local_lipschitz_representative line 103

   Source documentation

   Differentiation of local ball averages gives a sharp Lipschitz representative on the inner ball. No amplitude bound is needed.

   theorem NoncollapsedRCD.local_lipschitz_representative
       {K : ℝ} {n : ℕ} (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n)
       {u G : Lp ℝ 2 (hausdorff n X)} (hG : IsRelaxedSlope (hausdorff n X) u G)
       (L : ℝ≥0) {p : X} {R : ℝ} (hR : 0 < R)
       (hGb : ∀ᵐ x ∂(hausdorff n X).restrict (ball p (8 * R)), G x ≤ L) :
       ∃ v : X → ℝ, LipschitzWith L v ∧
         u =ᵐ[(hausdorff n X).restrict (closedBall p R)] v := by
   …

   Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.IsRelaxedSlope