OAI/Analysis/JiangSu/Comparison/ExactLocalSupply.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectComparison.corner_cutoff_coe line 15
2. lemma OAI.DirectComparison.corner_cutoff_fixes_cutoff line 27
3. lemma OAI.DirectComparison.exact_local_projection line 54
4. def OAI.DirectComparison.smallHat line 120
5. def OAI.DirectComparison.wideHat line 121
6. lemma OAI.DirectComparison.smallHat_cont line 122
7. lemma OAI.DirectComparison.wideHat_cont line 123
8. lemma OAI.DirectComparison.smallHat_bounds line 124
9. lemma OAI.DirectComparison.wideHat_bounds line 128
10. lemma OAI.DirectComparison.smallHat_supported line 130
11. lemma OAI.DirectComparison.wideHat_supported line 136
12. lemma OAI.DirectComparison.corner_smallHat_lower line 142
13. lemma OAI.DirectComparison.real_smul_mono_nonneg line 160
14. lemma OAI.DirectComparison.good_column_projection line 169
15. theorem OAI.DirectComparison.orthogonal_insertion line 199