OAI/Analysis/RieszRectifiability/Kernel/KernelNear.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Near-field inverse-distance estimates

Inner dyadic annuli turn upper growth of order p + 1 into a summable bound for the inverse-distance power of order p. The center has zero measure, so the annular estimates give integrability and a quantitative bound on the closed ball.

  1. theorem OAI.RieszRectifiability.dyadic_near_coefficient line 21
  2. theorem OAI.RieszRectifiability.inverseDistancePow_inner_annular_bound line 39
  3. theorem OAI.RieszRectifiability.inverseDistancePow_near_integrable_and_bound line 64
  4. theorem OAI.RieszRectifiability.inverseDistancePow_near_integral_bound line 95