OAI/Analysis/RieszRectifiability/Kernel/KernelBasic.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Elementary measurability and inverse-distance bounds for the Euclidean Riesz kernel. Global upper growth records the ball-mass estimate used in kernel integration.

  1. def OAI.RieszRectifiability.GlobalUpperGrowth line 18
  2. theorem OAI.RieszRectifiability.kernel_measurable_right line 22
  3. theorem OAI.RieszRectifiability.kernel_norm_of_ne line 30
  4. theorem OAI.RieszRectifiability.kernel_norm_le_truncation line 37
  5. def OAI.RieszRectifiability.inverseDistancePow line 45
  6. theorem OAI.RieszRectifiability.inverseDistancePow_measurable line 48
  7. theorem OAI.RieszRectifiability.inverseDistancePow_nonneg line 53