OAI/Analysis/OperatorAlgebra/VectorLpProjection.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Concrete spectral interval projections on vector-valued L².

  1. lemma OAI.WeakPureInfiniteness.indicator_bound line 16
  2. def OAI.WeakPureInfiniteness.vectorLpProjection line 20
  3. lemma OAI.WeakPureInfiniteness.vectorLpProjection_ae line 25
  4. lemma OAI.WeakPureInfiniteness.vectorLpProjection_norm_le line 34
  5. lemma OAI.WeakPureInfiniteness.vectorLpProjection_mul line 43
  6. lemma OAI.WeakPureInfiniteness.vectorLpProjection_star line 58
  7. lemma OAI.WeakPureInfiniteness.vectorLpProjection_isStarProjection line 69
  8. def OAI.WeakPureInfiniteness.vectorIntervalCutoff line 75
  9. lemma OAI.WeakPureInfiniteness.vectorIntervalCutoff_norm line 83
  10. lemma OAI.WeakPureInfiniteness.vectorIntervalCutoff_tendsto line 89
  11. lemma OAI.WeakPureInfiniteness.vectorIntervalCutoff_strong line 101