OAI/Analysis/RieszRectifiability/Kernel/L2Pairings.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Integral pairings of real L² functions

The L² inner product agrees with integration of pointwise products. Subtraction and Cauchy–Schwarz then bound differences of pairings by squared L² errors.

  1. theorem OAI.RieszRectifiability.real_scalar_inner_mul line 21
  2. theorem OAI.RieszRectifiability.toLp_inner_eq_integral line 26
  3. theorem OAI.RieszRectifiability.integral_mul_cauchy_schwarz_sq line 34
  4. theorem OAI.RieszRectifiability.integral_mul_sub_eq line 42
  5. theorem OAI.RieszRectifiability.integral_pairing_difference_sq_le line 51
  6. theorem OAI.RieszRectifiability.L2_pairing_tendsto line 58