OAI/Analysis/RieszRectifiability/Limits/CompactLimitGrowth.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Ball-mass bounds through compact test functions

Compactly supported continuous cutoffs compare test integrals with ball masses from above and below. These comparisons pass uniform growth bounds through convergence against compact test functions.

  1. theorem OAI.RieszRectifiability.compact_test_integral_le_ball_mass line 22
  2. theorem OAI.RieszRectifiability.ball_mass_le_compact_test_integral line 38
  3. theorem OAI.RieszRectifiability.compactTestConvergence_upper_growth line 54