OAI/Analysis/Commutator/FiniteFunctionalFactorization.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.OperatorFunctionals.coefficientDual line 20
2. lemma OAI.Kadison.OperatorFunctionals.coefficientDual_apply line 23
3. def OAI.Kadison.OperatorFunctionals.coefficient line 26
4. lemma OAI.Kadison.OperatorFunctionals.inner_coefficient line 50
5. lemma OAI.Kadison.OperatorFunctionals.eq_sum_coefficients line 57
6. lemma OAI.Kadison.OperatorFunctionals.norm_sq_sum_of_orthogonal line 67
7. lemma OAI.Kadison.OperatorFunctionals.inner_normalized_of_ne line 80
8. lemma OAI.Kadison.OperatorFunctionals.orthogonalColumn_norm_le line 88
9. lemma OAI.Kadison.OperatorFunctionals.orthogonalColumn_apply_basis line 107
10. def OAI.Kadison.OperatorFunctionals.singularBasis line 114
11. lemma OAI.Kadison.OperatorFunctionals.singularBasis_orthogonal line 118
12. lemma OAI.Kadison.OperatorFunctionals.norm_inv_smul_norm_le_one line 131
13. lemma OAI.Kadison.OperatorFunctionals.inner_norm_inv_smul line 138
14. lemma OAI.Kadison.OperatorFunctionals.sum_singular_coefficients_le line 148
15. lemma OAI.Kadison.OperatorFunctionals.balanced_inner line 170
16. lemma OAI.Kadison.OperatorFunctionals.balanced_right_norm_sq line 179
17. lemma OAI.Kadison.OperatorFunctionals.balanced_left_norm_sq line 188
18. theorem OAI.Kadison.OperatorFunctionals.exists_finite_factorization line 192