OAI/Geometry/RCD/Sobolev/SmallBallPoissonQuadratic.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.actual_poisson_small_ball_quadratic_error line 19

   Source documentation

   This is the quantitative quadratic-error field needed by the uniform sharp-projection family, derived from the full source budget and metric approximation of the actual coordinate representatives.

   theorem actual_poisson_small_ball_quadratic_error {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) (hε : 0 ≤ ε)
       (htheta : 0 < theta) (htheta4 : theta ≤ 1 / 4)
       (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))
   …

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