OAI/Analysis/RieszRectifiability/Kernel/CutoffTestMoments.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Moments of squared-cutoff tests

A cutoff bounded by one preserves square-integrability when its square multiplies a test function. Hölder integrability and pointwise domination then control the first moment of this test and its pairing with the original function.

  1. theorem OAI.RieszRectifiability.cutoff_square_le_one line 21
  2. theorem OAI.RieszRectifiability.squared_cutoff_test_memLp line 25
  3. theorem OAI.RieszRectifiability.squared_cutoff_test_moment_bounds line 35