OAI/Analysis/RieszRectifiability/Packing/VectorBesselTransfer.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Transferring scalar Bessel bounds to vector fields

Scalar-vector pairings commute with the Bochner integral, and the squared native L² norm agrees with the integral of the squared pointwise norm. Expanding in an orthonormal basis transfers a finite scalar Bessel bound to pairings of a vector field against test vectors of norm at most one, with the same Bessel constant.

  1. theorem OAI.RieszRectifiability.memLp_inner_const_of_vector line 22
  2. theorem OAI.RieszRectifiability.integral_scalar_vector_pairing line 29
  3. theorem OAI.RieszRectifiability.toLp_vector_norm_sq_eq_integral line 37
  4. theorem OAI.RieszRectifiability.vector_sq_integral_of_native_norm_bound line 46
  5. theorem OAI.RieszRectifiability.finite_vector_bessel_of_scalar line 61