OAI/NumberTheory/PiExponent/Approximation/AdmissibleMatrixInterpolation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponent.AdmissibleMatrixInterpolation.degreeWeights_eq_matrix line 14
2. theorem OAI.PiExponent.AdmissibleMatrixInterpolation.jetWeights_eq_matrix line 24
3. theorem OAI.PiExponent.AdmissibleMatrixInterpolation.actual_truncation_weight_bound line 34
4. theorem OAI.PiExponent.AdmissibleMatrixInterpolation.matrix_degree_of_supportBound line 62
5. theorem OAI.PiExponent.AdmissibleMatrixInterpolation.actualMatrix_surjective_of_formalPackets line 76
6. def OAI.PiExponent.AdmissibleMatrixInterpolation.WeightedPolynomials line 96
7. def OAI.PiExponent.AdmissibleMatrixInterpolation.packetMap line 101
8. theorem OAI.PiExponent.AdmissibleMatrixInterpolation.packetMap_surjective_of_family line 105
9. theorem OAI.PiExponent.AdmissibleMatrixInterpolation.actualMatrix_surjective_of_packetMap line 117
10. theorem OAI.PiExponent.AdmissibleMatrixInterpolation.cofinal_actualMatrix_of_eventual_packets line 127
11. theorem OAI.PiExponent.AdmissibleMatrixInterpolation.globalInterpolation_of_eventual_packets line 140