OAI/Analysis/Commutator/DihedralFejer.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.DihedralCorner.star_pow_mul_pow line 22
2. lemma OAI.Kadison.DihedralCorner.testPolynomial_expansion line 26
3. lemma OAI.Kadison.DihedralCorner.testPolynomial_reflection_commute line 37
4. def OAI.Kadison.DihedralCorner.compressCorner line 55
5. lemma OAI.Kadison.DihedralCorner.compressCorner_coe line 66
6. lemma OAI.Kadison.DihedralCorner.compressCorner_one line 68
7. lemma OAI.Kadison.DihedralCorner.compressCorner_wave line 73
8. def OAI.Kadison.DihedralCorner.fejerCorner line 76
9. lemma OAI.Kadison.DihedralCorner.fejerCorner_mem line 79
10. lemma OAI.Kadison.DihedralCorner.fejerCorner_selfAdjoint line 89
11. lemma OAI.Kadison.DihedralCorner.fejerCorner_coe_right line 97
12. lemma OAI.Kadison.DihedralCorner.fejerCorner_norm_le line 107
13. lemma OAI.Kadison.DihedralCorner.testPolynomial_reflection_trace line 137
14. lemma OAI.Kadison.DihedralCorner.fejerCorner_wave_trace line 149
15. lemma OAI.Kadison.DihedralCorner.fejerCorner_centered line 165
16. lemma OAI.Kadison.DihedralCorner.fejerCorner_positive_coefficient line 177
17. lemma OAI.Kadison.DihedralCorner.corner_preGNS_norm line 188
18. lemma OAI.Kadison.DihedralCorner.fejerCorner_preGNS_norm line 198