OAI/Analysis/RieszRectifiability/Kernel/LocalRenormalizedRepresentative.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Local representatives of renormalized Riesz pairings

The far-field pairing is represented by the scalar far Riesz transform. Adding this transform to a local interior representative gives the renormalized pairing on supported Lipschitz tests and preserves local L² integrability.

  1. theorem OAI.RieszRectifiability.far_pairing_eq_scalarFarRieszTransform line 22
  2. theorem OAI.RieszRectifiability.local_renormalized_pairing_representation line 41