OAI/Analysis/RieszRectifiability/Kernel/BlowupScalarPairing.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Scalar Riesz pairings under blowup

Change of variables for normalized blowup measures transfers the near and far parts of the scalar Riesz pairing. Rescaling the localization ball and pulling back the test function gives the exact factor (r ^ n)⁻¹ in the pairing identity.

  1. theorem OAI.RieszRectifiability.blowupMeasure_integral line 22
  2. theorem OAI.RieszRectifiability.blowupMeasure_integral_prod_restrict line 32
  3. theorem OAI.RieszRectifiability.kernel_normalized line 51
  4. theorem OAI.RieszRectifiability.blowup_preimage_closedExterior line 59
  5. theorem OAI.RieszRectifiability.rieszScalarPairing_blowup line 68