OAI/Analysis/Commutator/FreeHankelEntries.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.FreeBlocks.two_scaled_sum line 22
2. lemma OAI.Kadison.FreeBlocks.projection_factor_trace line 38
3. lemma OAI.Kadison.FreeBlocks.halfCornerTrace_normalization line 48
4. lemma OAI.Kadison.FreeBlocks.halfCornerTrace_normalization_re line 57
5. lemma OAI.Kadison.FreeBlocks.normalized_dihedral_scalar line 63
6. theorem OAI.Kadison.FreeBlocks.finite_fejer_entry line 86