OAI/Combinatorics/EuclideanRamsey/DifferentialSplitting.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EuclideanRamsey.secondOperator line 21
2. lemma OAI.EuclideanRamsey.secondOperator_continuous line 25
3. lemma OAI.EuclideanRamsey.secondOperator_compact line 35
4. def OAI.EuclideanRamsey.scaleVertical line 46
5. lemma OAI.EuclideanRamsey.scaleVertical_apply line 56
6. lemma OAI.EuclideanRamsey.split_differential line 66
7. lemma OAI.EuclideanRamsey.haar_linear_change line 126
8. lemma OAI.EuclideanRamsey.compact_prod_mul line 143
9. lemma OAI.EuclideanRamsey.negative_product_sum_bound line 153
10. lemma OAI.EuclideanRamsey.product_negative_integral_bound line 169
11. lemma OAI.EuclideanRamsey.halfLaplacian_continuous line 213
12. lemma OAI.EuclideanRamsey.halfLaplacian_compact line 221
13. theorem OAI.EuclideanRamsey.exists_split_smoothing line 230