OAI/Analysis/RieszRectifiability/Kernel/FiniteRieszPairing.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Finite-measure truncated Riesz pairings

The scalar truncated kernel is measurable and bounded away from its singularity. Symmetrization expresses finite-measure pairings as interior double integrals, whose integrability yields convergence as the truncation scale tends to zero.

  1. def OAI.RieszRectifiability.scalarTruncatedKernel line 22
  2. theorem OAI.RieszRectifiability.scalarTruncatedKernel_measurable line 26
  3. theorem OAI.RieszRectifiability.scalarTruncatedKernel_bound line 34
  4. theorem OAI.RieszRectifiability.scalarTruncatedKernel_swap line 46
  5. theorem OAI.RieszRectifiability.truncated_inner_eq_scalar_integral line 56
  6. theorem OAI.RieszRectifiability.truncated_weighted_pair_integrable line 71
  7. theorem OAI.RieszRectifiability.finite_truncated_pairing_symmetrization line 82
  8. theorem OAI.RieszRectifiability.finite_truncated_pairing_tendsto_of_integrable line 126
  9. theorem OAI.RieszRectifiability.rieszInteriorIntegrand_integrable_of_lipschitz line 161
  10. theorem OAI.RieszRectifiability.finite_localized_pairing_limit line 181
  11. theorem OAI.RieszRectifiability.truncated_restriction_eq_indicator line 191