OAI/Analysis/RieszRectifiability/Packing/SchurBilinear.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Bilinear Schur estimates

A nonnegative symmetric kernel with uniformly bounded row integrals defines an integrable bilinear pairing on square-integrable functions. Factoring the kernel through its square root reduces the quantitative bound to Cauchy–Schwarz on the product measure.

  1. theorem OAI.RieszRectifiability.schur_bilinear_integrable_and_sq_bound line 24