OAI/Analysis/RieszRectifiability/Limits/CompactRieszPairingTail.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Compactly supported pairing tails

Global upper growth bounds the integral of a bounded, compactly supported test function. This gives an explicit constant for the inverse-radius error between the scalar Riesz pairing and its interior product-measure integral.

  1. theorem OAI.RieszRectifiability.compact_supported_abs_integral_bound line 22
  2. def OAI.RieszRectifiability.compactRieszTailConstant line 55
  3. theorem OAI.RieszRectifiability.compactRieszTailConstant_nonneg line 59
  4. theorem OAI.RieszRectifiability.rieszScalarPairing_interior_tail_bound line 65