AlmostEuclideanSourceBudget.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Small full-source mass throughout an almost-Euclidean volume regime

theorem OAI.RegularPointCoordinates.normalized_volume_bounds line 13

theorem OAI.RegularPointCoordinates.DyadicDistanceSources.almost_euclidean_budget line 31

Source documentation

An actual dyadic distance source has a small total normalized mass under the same all-scale relative volume bounds used for the heat family.

theorem DyadicDistanceSources.almost_euclidean_budget {n : ℕ} {κ r0 omega epsilon : ℝ} {p : X}
    (D : DyadicDistanceSources μ hQ n κ p r0) (hn : 0 < n) (hκ : 0 ≤ κ)
    (homega : 0 < omega) (hepsilon : 0 ≤ epsilon)
    {model : ℝ → ℝ} (hBG : BallVolumeComparison μ model) (hmodel : Continuous model)
    (hmodelpos : ∀ r, 0 < r → 0 < model r)
    (hvolume : ∀ r, 0 < r → r ≤ r0 → |μ.real (ball p r) / (omega * r ^ n) - 1| ≤ epsilon) :
    Summable (normalizedDistanceSourceMass μ hQ D) ∧
      (∑' i, normalizedDistanceSourceMass μ hQ D i) ≤
        2 * (radialCutoffCoefficient (n : ℝ))⁻¹ * epsilon * omega +
          (4 * κ * r0 ^ 2 * ((1 + epsilon) * omega) * (2 : ℝ) ^ (n : ℝ)) * (4 / 3) := by
…

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