OAI/Geometry/RCD/Metric/DistanceSourceMeasure.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

One actual distance source supplies both replacement and mass bounds

  1. theorem OAI.RegularPointCoordinates.distance_source_and_volume_drop line 18

    Source documentation

    The published distance Laplacian constructs the source. The checked radial test then bounds that same source by the signed volume drop.

    theorem distance_source_and_volume_drop {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n)
    (hdistance : LocalSquaredDistanceInput hX)
    {κ r : ℝ} (hκ : 0 ≤ κ) (hK : -κ ≤ K) (p : X) (hr : 0 < r)
    {model : ℝ → ℝ} (hBG : BallVolumeComparison (hausdorff n X) model)
    (hmodel : Continuous model) (hmodelr : 0 < model r) :
    letI : IsLocallyFiniteMeasure (hausdorff n X) :=
…

    Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.LocalSquaredDistanceInput, OAI.RegularPointCoordinates.BallVolumeComparison, OAI.RegularPointCoordinates.hausdorff