OAI/Analysis/JiangSu/DimensionDrop/DimensionDrop.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JiangSuConstruction.scalarMatrix line 19
2. lemma OAI.JiangSuConstruction.scalarMatrix_mem line 22
3. def OAI.JiangSuConstruction.interiorMatrix line 31
4. lemma OAI.JiangSuConstruction.interiorMatrix_norm_le line 35
5. lemma OAI.JiangSuConstruction.interiorMatrix_norm_eq line 47
6. lemma OAI.JiangSuConstruction.matrix_unit_norm line 73
7. lemma OAI.JiangSuConstruction.matrix_unit_compress line 78
8. lemma OAI.JiangSuConstruction.exists_interior_bump line 87
9. lemma OAI.JiangSuConstruction.complex_smul_real line 103
10. lemma OAI.JiangSuConstruction.scalarMatrix_apply_complex line 107
11. lemma OAI.JiangSuConstruction.interior_compression_error line 110