OAI/Analysis/RieszRectifiability/Kernel/VectorL2PairingBounds.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A vector-valued L² norm estimate controls each scalar pairing against a fixed direction. The proof combines pointwise inner-product bounds with the L² Cauchy–Schwarz inequality.

  1. theorem OAI.RieszRectifiability.toLp_norm_eq_sqrt_integral line 18
  2. theorem OAI.RieszRectifiability.scalar_L2_pairing_of_vector_norm_bound line 23