OAI/Analysis/RieszRectifiability/Rigidity/ReflectionlessAnnularBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Annular bounds from scalar reflectionlessness

Scalar reflectionlessness annihilates localized pairings against mean-zero test functions. Comparing normalized bumps at two radii bounds centered annular kernel integrals, first in each scalar direction and then in the ambient Euclidean norm.

  1. def OAI.RieszRectifiability.ScalarReflectionlessAt line 22
  2. theorem OAI.RieszRectifiability.reflectionless_centered_annular_scalar_bound line 28
  3. theorem OAI.RieszRectifiability.reflectionless_centered_annular_vector_bound line 98