OAI/Analysis/OperatorAlgebra/ScalarLpCutoffConvergence.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The interval spectral cutoffs on scalar L² converge strongly to the identity, giving a strongly exhausting family of projections.

  1. lemma OAI.WeakPureInfiniteness.scalarLp_norm_sq_integral line 14
  2. def OAI.WeakPureInfiniteness.scalarIntervalProjection line 26
  3. lemma OAI.WeakPureInfiniteness.scalarIntervalProjection_ae line 30
  4. lemma OAI.WeakPureInfiniteness.scalarIntervalProjection_norm_le line 34
  5. lemma OAI.WeakPureInfiniteness.scalarIntervalProjection_isStarProjection line 37
  6. lemma OAI.WeakPureInfiniteness.scalarIntervalProjection_strong line 41