OAI/Analysis/RieszRectifiability/Kernel/ExteriorDilationIntegrability.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Integrability under dilation of exterior regions

Positive dilation identifies the unit closed exterior with the closed exterior at the dilation radius. This change of variables transports integrability of functions on exterior regions to their rescaled compositions.

  1. theorem OAI.RieszRectifiability.preimage_closedExterior_dilation line 20
  2. theorem OAI.RieszRectifiability.integrableOn_closedExterior_comp_smul line 27
  3. theorem OAI.RieszRectifiability.exterior_weighted_normalized_dilation_integrable line 42