SmallBallPoissonValue.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Poisson value errors on the smaller balls used by two-center transport

theorem OAI.RegularPointCoordinates.relative_ball_volume_ratio line 13

theorem OAI.RegularPointCoordinates.rcd_poisson_small_ball_value_error_le line 46

Source documentation

The same actual source budget controls every fixed smaller interior ball; the explicit volume loss is the only dependence on its radius ratio.

theorem rcd_poisson_small_ball_value_error_le {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n)
    [IsFiniteMeasureOnCompacts (hausdorff n X)]
    {κ r0 B J C omega eta theta : ℝ} {p : X}
    {S : DyadicDistanceSources (hausdorff n X) hX.quadratic n κ p r0}
    (T : DyadicDistanceReplacements (hausdorff n X) hX.quadratic S B J C)
    (hκ : 0 ≤ κ) (hB : 0 ≤ B) (heta : 0 ≤ eta)
    (htheta : 0 < theta) (htheta1 : theta ≤ 1) (hr01 : r0 ≤ 1) (homega : 0 < omega)
    (hvol : ∀ r : ℝ, 0 < r → r ≤ r0 →
      |(hausdorff n X).real (ball p r) / (omega * r ^ n) - 1| ≤ 1 / 4)
    (hsum : Summable (normalizedPoissonDefect (hausdorff n X) hX.quadratic S))
    (hbudget : (∑' j, normalizedPoissonDefect (hausdorff n X) hX.quadratic S j) ≤ eta)
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.DyadicDistanceSources, OAI.RegularPointCoordinates.DyadicDistanceReplacements, OAI.RegularPointCoordinates.normalizedPoissonDefect