OAI/Analysis/OperatorAlgebra/ScalarLpStrongConvergence.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Bounded pointwise convergence of actual scalar multipliers gives strong operator convergence. Commutation consequently passes to their strong limits. These lemmas are used to obtain measurable cutoffs from continuous calculus.

  1. lemma OAI.WeakPureInfiniteness.boundedScalarLp_strong line 15
  2. lemma OAI.WeakPureInfiniteness.scalarLpRepresentation_strong line 68
  3. lemma OAI.WeakPureInfiniteness.commute_of_strong_limit line 89