OAI/Analysis/JiangSu/DimensionDrop/DimensionDropTensorCoefficients.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.JiangSuConstruction.tensor_norm_sum_le line 21
2. lemma OAI.JiangSuConstruction.tensor_norm_compress_le line 30
3. lemma OAI.JiangSuConstruction.interior_tensor_coefficient_le line 54
4. lemma OAI.JiangSuConstruction.tensor_coefficient_le line 111
5. lemma OAI.JiangSuConstruction.matrix_unit_expansion line 136
6. lemma OAI.JiangSuConstruction.scalarMatrix_norm_le line 141
7. def OAI.JiangSuConstruction.cutoffAmplification line 148
8. lemma OAI.JiangSuConstruction.cutoffAmplification_norm_le line 176
9. lemma OAI.JiangSuConstruction.tensor_basis_bound line 181
10. lemma OAI.JiangSuConstruction.tensor_cutoff_bound line 211