PoissonDefectBudget.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The summable defect including the Poisson curvature remainder

theorem OAI.RegularPointCoordinates.distanceSourceRadius_sq line 13
def OAI.RegularPointCoordinates.normalizedPoissonDefect line 23
Source documentation
The second term is the actual curvature remainder in the shifted Poisson mass estimate, in the same normalized units as the full source.
```
def normalizedPoissonDefect {n : ℕ} {κ r0 : ℝ} {p : X}
    (S : DyadicDistanceSources μ hQ n κ p r0) (i : ℕ) : ℝ :=
…
```
Mentions: OAI.RegularPointCoordinates.DyadicDistanceSources
theorem OAI.RegularPointCoordinates.normalizedPoissonDefect_nonneg line 28
theorem OAI.RegularPointCoordinates.normalizedPoissonDefect_units line 37
Source documentation
Source and curvature masses have exactly the same normalization; the identity uses the actual volume, not a Euclidean replacement.
```
theorem normalizedPoissonDefect_units {n : ℕ} {κ r0 : ℝ} {p : X}
    (S : DyadicDistanceSources μ hQ n κ p r0) (i : ℕ) :
    (distanceSourceRadius r0 i) ^ (n : ℝ) * normalizedPoissonDefect μ hQ S i =
      (S.source i).real (ball p (distanceSourceRadius r0 i)) +
        κ * (distanceSourceRadius r0 i) ^ 2 * μ.real (ball p (distanceSourceRadius r0 i)) := by
…
```
Mentions: OAI.RegularPointCoordinates.DyadicDistanceSources, OAI.RegularPointCoordinates.distanceSourceRadius, OAI.RegularPointCoordinates.normalizedPoissonDefect

theorem OAI.RegularPointCoordinates.DyadicDistanceSources.poisson_defect_budget line 50

Source documentation

The extra curvature remainder costs at most kappa*C*r0²/3 in the total budget. The original positive source measures remain unchanged.

theorem DyadicDistanceSources.poisson_defect_budget {n : ℕ} {κ r0 C : ℝ} {p : X}
    (S : DyadicDistanceSources μ hQ n κ p r0) (hκ : 0 ≤ κ) (hC : 0 ≤ C)
    (hsource : Summable (normalizedDistanceSourceMass μ hQ S))
    (hvolume : ∀ i, (distanceSourceRadius r0 i) ^ (-(n : ℝ)) *
      μ.real (ball p (distanceSourceRadius r0 i)) ≤ C) :
    Summable (normalizedPoissonDefect μ hQ S) ∧
      (∑' i, normalizedPoissonDefect μ hQ S i) ≤
        (∑' i, normalizedDistanceSourceMass μ hQ S i) + κ * C * r0 ^ 2 / 3 := by
…

Mentions: OAI.RegularPointCoordinates.DyadicDistanceSources, OAI.RegularPointCoordinates.normalizedDistanceSourceMass, OAI.RegularPointCoordinates.distanceSourceRadius, OAI.RegularPointCoordinates.normalizedPoissonDefect