OAI/Analysis/RieszRectifiability/Kernel/ADTruncations.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Hard truncations for AD-regular measures

For support of infinite diameter, AD regularity yields global upper growth. For bounded support, the measure is finite. These two cases establish integrability of every positive hard truncation against an L² input without imposing boundedness on the support.

  1. theorem OAI.RieszRectifiability.adRegular_globalGrowth_of_ediam_top line 21
  2. theorem OAI.RieszRectifiability.finiteMeasure_of_bounded_support line 47
  3. theorem OAI.RieszRectifiability.truncation_integrable_of_ADRegular line 60