OAI/Analysis/RieszRectifiability/Packing/OriginalVectorTestBessel.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Vector-valued Bessel estimates for dyadic oscillation tests

The scalar Bessel estimate transfers through the Euclidean orthonormal basis to directional pairings with vector-valued L² functions. The normalization retains the radius powers and interaction-packing constant, and the resulting estimate applies to the hard-truncated Riesz transform under its L² bound.

  1. theorem OAI.RieszRectifiability.DyadicOscillationTests.vector_bessel line 23
  2. theorem OAI.RieszRectifiability.DyadicOscillationTests.native_truncation_bessel line 42