OAI/Analysis/Pureness/Operators/FiniteHilbertFrames.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.finiteFrameSynthesis line 11
2. lemma OAI.CuntzPureness.finiteFrameSynthesis_apply line 14
3. lemma OAI.CuntzPureness.finiteFrameSynthesis_standard line 18
4. lemma OAI.CuntzPureness.finiteFrameSynthesis_adjoint line 24
5. lemma OAI.CuntzPureness.finiteFrameSynthesis_adjoint_apply line 29
6. lemma OAI.CuntzPureness.orthonormal_standardFinite line 33
7. theorem OAI.CuntzPureness.finiteFrameSynthesis_norm_le line 39
8. lemma OAI.CuntzPureness.finiteFrameSynthesis_adjoint_norm_le line 54
9. theorem OAI.CuntzPureness.finiteFrame_compression line 58