DistanceSourceBudget.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Summability of the constructed distance sources from volume bounds

def OAI.RegularPointCoordinates.distanceVolumeProfile line 18
def OAI.RegularPointCoordinates.normalizedDistanceSourceMass line 21
theorem OAI.RegularPointCoordinates.distanceVolumeProfile_succ line 26
theorem OAI.RegularPointCoordinates.DyadicDistanceSources.normalized_mass_le line 33

theorem OAI.RegularPointCoordinates.DyadicDistanceSources.mass_budget line 56

Source documentation

The full source masses are summable even when the raw Euclidean volume profile is not monotone. The only volume input is its upper bound.

theorem DyadicDistanceSources.mass_budget {n : ℕ} {κ r0 C : ℝ} {p : X}
    (D : DyadicDistanceSources μ hQ n κ p r0) (hn : 0 < n) (hκ : 0 ≤ κ) (hC : 0 ≤ C)
    {model : ℝ → ℝ} (hBG : BallVolumeComparison μ model) (hmodel : Continuous model)
    (hmodelpos : ∀ r, 0 < r → 0 < model r)
    (hupper : ∀ i, distanceVolumeProfile μ n p r0 i ≤ C) :
    Summable (normalizedDistanceSourceMass μ hQ D) ∧
      (∑' i, normalizedDistanceSourceMass μ hQ D i) ≤
        (radialCutoffCoefficient (n : ℝ))⁻¹ * (C - distanceVolumeProfile μ n p r0 0) +
          (4 * κ * r0 ^ 2 * C * (2 : ℝ) ^ (n : ℝ)) * (4 / 3) := by
…

Mentions: OAI.RegularPointCoordinates.DyadicDistanceSources, OAI.RegularPointCoordinates.BallVolumeComparison, OAI.RegularPointCoordinates.distanceVolumeProfile, OAI.RegularPointCoordinates.normalizedDistanceSourceMass, OAI.RegularPointCoordinates.radialCutoffCoefficient