OAI/Analysis/JiangSu/Nuclearity/NuclearUnitization.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.NuclearUnitization.restrictNorm line 19
2. lemma OAI.NuclearUnitization.nuclear_restriction_eq line 34
3. lemma OAI.NuclearUnitization.norm_one_sub_inr line 42
4. lemma OAI.NuclearUnitization.tensor_approx_unit_defect line 53
5. lemma OAI.NuclearUnitization.scalar_part_bound line 71
6. lemma OAI.NuclearUnitization.nuclear_norm_bound line 99
7. theorem OAI.NuclearUnitization.nuclear_unitization line 113