OAI/Analysis/Commutator/L2FiniteSum.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.Decomposable.memLp_vector line 22
2. def OAI.Kadison.Decomposable.assemble line 27
3. lemma OAI.Kadison.Decomposable.assemble_ae line 31
4. lemma OAI.Kadison.Decomposable.assemble_add line 35
5. lemma OAI.Kadison.Decomposable.assemble_smul line 48
6. lemma OAI.Kadison.Decomposable.assemble_norm line 61
7. def OAI.Kadison.Decomposable.assembleIsometry line 73
8. lemma OAI.Kadison.Decomposable.assemble_surjective line 80
9. def OAI.Kadison.Decomposable.finiteSumEquiv line 93