OAI/Analysis/RieszRectifiability/Kernel/SourceRadialCutoffMass.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Lower mass bounds for radial cutoffs

A radial cutoff equal to one on a smaller ball transfers its mass lower bound to the squared-cutoff integral on a larger ball. For source measures with growing support diameters, the prescribed lower growth estimate supplies this bound eventually.

  1. theorem OAI.RieszRectifiability.radial_cutoff_mass_of_ball_mass line 21
  2. theorem OAI.RieszRectifiability.source_radial_cutoff_mass_eventually line 44