OAI/Analysis/JiangSu/Comparison/HatPartition.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DirectComparison.unitIntervalClamp line 11
2. lemma OAI.DirectComparison.unitIntervalClamp_continuous line 12
3. lemma OAI.DirectComparison.unitIntervalClamp_mem line 14
4. lemma OAI.DirectComparison.unitIntervalClamp_eq line 16
5. theorem OAI.DirectComparison.exists_localized_partition line 20
6. lemma OAI.DirectComparison.trace_re_mono line 87
7. lemma OAI.DirectComparison.trace_re_nonneg line 91
8. def OAI.DirectComparison.ProjectionPacking.ScalarGood line 94
9. lemma OAI.DirectComparison.ProjectionPacking.empty_good line 97
10. lemma OAI.DirectComparison.ProjectionPacking.append_good line 99
11. lemma OAI.DirectComparison.ProjectionPacking.singleton_good line 107
12. lemma OAI.DirectComparison.uniform_moving_corner_bound line 112
13. lemma OAI.DirectComparison.sum_cornerCFC line 154
14. lemma OAI.DirectComparison.scalar_run line 168