OAI/Analysis/RieszRectifiability/Kernel/FiniteShellTail.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Weighted height bounds on dyadic shells

Square-integrable height bounds on each shell control integrals weighted by inverse powers of distance. The dyadic coefficient identity expresses these estimates in the geometric form needed for tail bounds.

  1. theorem OAI.RieszRectifiability.dyadic_weighted_height_coefficient line 21
  2. theorem OAI.RieszRectifiability.shell_weighted_height_integrable_and_bound line 27
  3. def OAI.RieszRectifiability.finiteShellRegion line 59
  4. theorem OAI.RieszRectifiability.finiteShellRegion_eq line 62
  5. theorem OAI.RieszRectifiability.finite_shell_weighted_height_bound line 84