OAI/Analysis/RieszRectifiability/Limits/SignedKernelConvergence.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Convergence of signed weighted kernel integrals

Finite step approximations in the second variable reduce weighted product integrals to sums of weighted moments and cell masses. Integrable absolute weights and Lipschitz kernel bounds control the approximation error, allowing convergence of these finite sums to pass to the original kernel integrals.

  1. theorem OAI.RieszRectifiability.integrable_weighted_bounded_function line 25
  2. theorem OAI.RieszRectifiability.integrable_weighted_product_kernel line 35
  3. def OAI.RieszRectifiability.secondVariableStep line 49
  4. theorem OAI.RieszRectifiability.weighted_secondVariableStep_eq_sum line 53
  5. theorem OAI.RieszRectifiability.integrable_weighted_secondVariableStep line 66
  6. theorem OAI.RieszRectifiability.integral_weighted_secondVariableStep line 79
  7. theorem OAI.RieszRectifiability.weighted_secondVariableStep_error line 99
  8. theorem OAI.RieszRectifiability.weighted_product_kernel_tendsto line 140