OAI/Combinatorics/MatchingPSD/ScalarSmoothing.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatchingSmoothing.eventually_power_le_choose line 8
2. lemma OAI.MatchingSmoothing.eventually_table_moment_small line 17
3. def OAI.MatchingSmoothing.polynomialProjection line 38
4. lemma OAI.MatchingSmoothing.residual_mem_high line 41
5. lemma OAI.MatchingSmoothing.residual_norm_le line 45
6. lemma OAI.MatchingSmoothing.uniform_table_smoothing line 50