OAI/Analysis/RieszRectifiability/Kernel/TruncationIntegrability.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Integrability of hard Riesz truncations

Global upper growth makes the Riesz kernel square-integrable outside each positive-radius ball. Pairing this exterior estimate with an L² input proves integrability of the hard truncation. For finite measures, integrability instead follows from the bounded exterior kernel and the inclusion of L² in L¹.

  1. theorem OAI.RieszRectifiability.kernel_sq_norm_le_tail_weight line 22
  2. theorem OAI.RieszRectifiability.kernel_memLp_two_on_exterior line 33
  3. theorem OAI.RieszRectifiability.truncation_integrable_of_globalGrowth line 48
  4. theorem OAI.RieszRectifiability.truncation_integrable_of_finiteMeasure line 56