OAI/Analysis/RieszRectifiability/Kernel/RenormalizedFarPairing.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.RieszRectifiability.inverseDistancePow_far_leline 13 - def
OAI.RieszRectifiability.renormalizedNormalIntegrandline 27 - theorem
OAI.RieszRectifiability.renormalizedNormalIntegrand_boundline 32 - theorem
OAI.RieszRectifiability.renormalizedNormalIntegrand_bound_of_supportline 64 - theorem
OAI.RieszRectifiability.renormalized_far_pairing_integrable_and_boundline 75