OAI/Analysis/JiangSu/Nonunital/RelativeCoefficient.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.NonunitalRelative.coefficient_transfer line 22
2. lemma OAI.NonunitalRelative.unitary_conjugate_inclusion line 45
3. def OAI.NonunitalRelative.coefficientSum line 66
4. def OAI.NonunitalRelative.originalSum line 68
5. def OAI.NonunitalRelative.coefficientBound line 71
6. lemma OAI.NonunitalRelative.coefficientBound_nonneg line 74
7. lemma OAI.NonunitalRelative.finite_coefficient_control line 77
8. theorem OAI.NonunitalRelative.finite_coefficient_approximation line 120