OAI/Analysis/OperatorAlgebra/VectorLpStrongConvergence.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Strong convergence of scalar multipliers on vector-valued L². This is used to put frequency cutoffs and Gaussian regularizers into the actual modular core.

  1. lemma OAI.WeakPureInfiniteness.vectorLp_norm_sq_integral line 18
  2. lemma OAI.WeakPureInfiniteness.boundedVectorLp_strong line 31
  3. lemma OAI.WeakPureInfiniteness.vectorLpRepresentation_strong line 82