OAI/Analysis/JiangSu/Excision/ExcisionCoefficientAssembly.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CStarExcision.assembled line 18
2. def OAI.CStarExcision.coefficientValue line 19
3. lemma OAI.CStarExcision.assembled_square line 22
4. lemma OAI.CStarExcision.coefficient_mul line 33
5. lemma OAI.CStarExcision.assembly_error_identity line 48
6. theorem OAI.CStarExcision.assembly_error_le line 61
7. theorem OAI.CStarExcision.compression_error_le line 90
8. lemma OAI.DirectComparison.cut_rank_lower_from_trace line 133
9. theorem OAI.DirectComparison.small_trace_supported_isometry line 146
10. theorem OAI.DirectComparison.supported_state_excision line 181