OAI/Analysis/OperatorAlgebra/GNSSeparatingSequence.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

A concrete square-summable separating vector for the countable diagonal amplification. Its zeroth coordinate is the prescribed vector.

  1. def OAI.WeakPureInfiniteness.separatingSequenceWeight line 15
  2. lemma OAI.WeakPureInfiniteness.separatingSequenceWeight_pos line 19
  3. def OAI.WeakPureInfiniteness.separatingSequenceTerm line 24
  4. lemma OAI.WeakPureInfiniteness.separatingSequenceTerm_norm_le line 28
  5. lemma OAI.WeakPureInfiniteness.separatingSequenceTerm_norm_summable line 40
  6. lemma OAI.WeakPureInfiniteness.sequenceEval_apply line 46
  7. lemma OAI.WeakPureInfiniteness.separatingSequenceTerm_summable line 49
  8. def OAI.WeakPureInfiniteness.separatingSequence line 53
  9. lemma OAI.WeakPureInfiniteness.separatingSequence_zero line 56
  10. lemma OAI.WeakPureInfiniteness.separatingSequence_succ line 64
  11. lemma OAI.WeakPureInfiniteness.separatingSequence_norm_le line 77
  12. lemma OAI.WeakPureInfiniteness.separatingSequence_separates line 91
  13. lemma OAI.WeakPureInfiniteness.sequence_bicommutant_separating line 111