OAI/Analysis/RieszRectifiability/Kernel/RieszPairingMeanCorrection.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Mean corrections for localized Riesz pairings

Subtracting the center kernel separates a far-field pairing into its renormalized part and a correction proportional to the test function's integral. Comparing localization radii expresses their difference through this mean and a shell integral.

  1. theorem OAI.RieszRectifiability.riesz_far_integral_with_mean_correction line 21
  2. theorem OAI.RieszRectifiability.finite_pairing_eq_renormalized_with_mean line 43
  3. theorem OAI.RieszRectifiability.finite_rieszScalarPairing_radius_difference line 62
  4. theorem OAI.RieszRectifiability.rieszScalarPairing_radius_difference line 87
  5. theorem OAI.RieszRectifiability.rieszScalarPairing_sub_of_integrable line 140