OAI/Analysis/RieszRectifiability/Packing/ADTestFamilyBessel.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Bessel estimate for dyadic Lipschitz test families

Summable bounds on the scale slices of the Gram matrix give a Bessel inequality for finite families of test functions under upper growth and lower AD bounds. The resulting constant depends explicitly on the interaction packing estimate.

  1. theorem OAI.RieszRectifiability.DyadicLipschitzFamily.bessel line 21
  2. theorem OAI.RieszRectifiability.DyadicLipschitzFamily.packing_of_large_pairings line 84