OAI/Analysis/RieszRectifiability/Kernel/HardBilinearPairing.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Bilinear pairings for hard truncations

Integrability of bounded-kernel products permits the product-space bilinear form to be rewritten as a pairing with the hard-truncated Riesz transform. This identification connects kernel integrals with the vector-valued L² estimates.

  1. theorem OAI.RieszRectifiability.bounded_kernel_bilinear_integrable line 22
  2. theorem OAI.RieszRectifiability.truncated_inner_eq_weighted_scalar_integral line 34
  3. theorem OAI.RieszRectifiability.hard_bilinear_eq_truncated_pairing line 54
  4. theorem OAI.RieszRectifiability.hard_bilinear_bound_of_native_L2 line 71