PoissonValueLimit.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

RCD Poisson value convergence in the established volume regime

theorem OAI.RegularPointCoordinates.rcd_poisson_value_tendsto_zero line 19

Source documentation

The quarter-error volume regime supplies the annular Poincare constant and lower volume bound needed for the actual Poisson value limit.

theorem rcd_poisson_value_tendsto_zero {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n)
    [IsFiniteMeasureOnCompacts (hausdorff n X)]
    {κ r0 B J C omega : ℝ} {p : X}
    {S : DyadicDistanceSources (hausdorff n X) hX.quadratic n κ p r0}
    (T : DyadicDistanceReplacements (hausdorff n X) hX.quadratic S B J C)
    (hB : 0 ≤ B) (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)
    (hmass : Summable (normalizedDistanceSourceMass (hausdorff n X) hX.quadratic S)) :
    Tendsto (fun i => ‖normalizeLocalL2 (hausdorff n X) (ball p (distanceSourceRadius r0 i))
      (ne_of_lt (hX.finiteOnBounded _ isBounded_ball))
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.DyadicDistanceSources, OAI.RegularPointCoordinates.DyadicDistanceReplacements, OAI.RegularPointCoordinates.normalizedDistanceSourceMass, OAI.RegularPointCoordinates.normalizeLocalL2, OAI.RegularPointCoordinates.distanceSourceRadius