OAI/Combinatorics/MatchingPSD/CommonSelection.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatchingSmoothing.mean_right_translate line 14
2. lemma OAI.MatchingSmoothing.mean_le_of_local_means line 19
3. lemma OAI.MatchingSmoothing.exists_total_le_of_local_means line 28