OAI/Analysis/RieszRectifiability/Limits/CompactRieszPairing.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Compactly supported Lipschitz Riesz pairings

Growth bounds control the exterior pairing of a compactly supported Lipschitz test. Finite ball restrictions then connect truncated pairings to the renormalized pairing through the outer-radius limit.

  1. theorem OAI.RieszRectifiability.rieszFarIntegrand_integrable_of_compact_lipschitz line 21
  2. theorem OAI.RieszRectifiability.native_pairing_eq_finite_localization line 48
  3. theorem OAI.RieszRectifiability.riesz_pairing_as_iterated_hard_limits line 59