OAI/Geometry/RCD/Sobolev/PoissonInteriorValues.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform Poisson values on the interior compactness ball

  1. theorem OAI.RegularPointCoordinates.quarter_volume_ratio line 14
  2. theorem OAI.RegularPointCoordinates.rcd_poisson_interior_value_error_le line 49

    Source documentation

    Restriction of the actual replacement to the interior quarter ball preserves a uniform error bound. Only the explicit Euclidean volume ratio is lost; the bound is independent of the center and dyadic index.

    theorem rcd_poisson_interior_value_error_le {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n)
    [IsFiniteMeasureOnCompacts (hausdorff n X)]
    {κ r0 B J C omega eta : ℝ} {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) (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)
    (i : ℕ) :
…

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