OAI/Combinatorics/MatchingPSD/MatrixInterpolation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatchingInterpolation.specialPoint line 12
2. def OAI.MatchingInterpolation.specialCoeff line 14
3. def OAI.MatchingInterpolation.scaledNode line 15
4. def OAI.MatchingInterpolation.weightMass line 17
5. lemma OAI.MatchingInterpolation.weightMass_nonneg line 19
6. lemma OAI.MatchingInterpolation.sum_abs_specialCoeff line 22
7. lemma OAI.MatchingInterpolation.five_interpolation line 25
8. lemma OAI.MatchingInterpolation.finite_weighted_error line 34
9. lemma OAI.MatchingInterpolation.interpolation_error line 46
10. lemma OAI.MatchingInterpolation.interpolation_matrix_domination line 71