OAI/Analysis/RieszRectifiability/Kernel/LocalTestMoments.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Local moments of bounded tests

Compact support makes products of mean-corrected tests with continuous height functions integrable. Local mass and square-integrability bounds then control the absolute moments of bounded tests and their height-weighted products.

  1. theorem OAI.RieszRectifiability.meanCorrection_height_product_integrable line 22
  2. theorem OAI.RieszRectifiability.bounded_test_local_moment_bounds line 30