OAI/Combinatorics/EuclideanRamsey/SmoothingMatrix.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.EuclideanRamsey.exists_positive_shift line 16
2. lemma OAI.EuclideanRamsey.covariance_splitting line 33
3. lemma OAI.EuclideanRamsey.positive_joint_pushforward line 61
4. theorem OAI.EuclideanRamsey.exists_small_covariance line 99
5. def OAI.EuclideanRamsey.stencilDifferential line 149
6. def OAI.EuclideanRamsey.gradientWeight line 154
7. lemma OAI.EuclideanRamsey.gradientWeight_nonneg line 157
8. def OAI.EuclideanRamsey.CompactSmoothing line 160
9. theorem OAI.EuclideanRamsey.compact_smoothing line 173