OAI/Analysis/RieszRectifiability/Kernel/NearBilinear.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Near-diagonal fractional bilinear bounds

On the near-pair region, Lipschitz control makes the test function's fractional energy integrable under upper growth. Cauchy–Schwarz then bounds the absolute bilinear pairing by the full energy of the other function and the near-pair inverse-distance integral.

  1. theorem OAI.RieszRectifiability.near_fractionalBilinear_integrable_and_bound line 22
  2. theorem OAI.RieszRectifiability.near_fractionalBilinear_absolute_bound line 81