OAI/Geometry/RCD/Sobolev/LocalAverageRepresentative.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Local Lipschitz representatives from shrinking-ball averages

  1. theorem OAI.RegularPointCoordinates.exists_lipschitz_of_local_average_bound line 19

    Source documentation

    The averaging estimate need only hold at sufficiently small radii for each pair of centers in the chosen region.

    theorem exists_lipschitz_of_local_average_bound (u : X → ℝ) (hu : LocallyIntegrable u μ)
    {S : Set X} (hS : MeasurableSet S) (L : ℝ≥0)
    (h : ∀ x ∈ S, ∀ y ∈ S, ∀ᶠ r in 𝓝[>] (0:ℝ),
      |(⨍ z in closedBall x r, u z ∂μ)-(⨍ z in closedBall y r, u z ∂μ)| ≤
        L*(dist x y+2*r)) :
    ∃ v : X → ℝ, LipschitzWith L v ∧ u =ᵐ[μ.restrict S] v := by
…