OAI/Combinatorics/Progressions/Polynomial/CRTPolynomialPatchComposition.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.PolynomialPatch.liftInterleaving line 12
  2. theorem OAI.Erdos3.PolynomialPatch.liftInterleaving_before line 17
  3. def OAI.Erdos3.PolynomialPatch.insertLifts line 23
  4. theorem OAI.Erdos3.PolynomialPatch.insertLifts_lip line 36
  5. theorem OAI.Erdos3.PolynomialPatch.insertLifts_term line 40
  6. theorem OAI.Erdos3.PolynomialPatch.insertLifts_contributing_lift line 55
  7. theorem OAI.Erdos3.PolynomialPatch.insertLifts_value_at_lift line 66
  8. theorem OAI.Erdos3.PolynomialPatch.insertLifts_value line 77
  9. def OAI.Erdos3.crtLiftPolynomial line 102
  10. theorem OAI.Erdos3.crtLiftPolynomial_degree line 107
  11. theorem OAI.Erdos3.crtLiftPolynomial_eval line 118
  12. def OAI.Erdos3.RepresentativeWindow.composeCRTPatch line 129
  13. theorem OAI.Erdos3.RepresentativeWindow.composeCRTPatch_lip line 141
  14. theorem OAI.Erdos3.RepresentativeWindow.composeCRTPatch_value line 144
  15. theorem OAI.Erdos3.RepresentativeWindow.composeCRTPatch_value_residues line 155
  16. theorem OAI.Erdos3.RepresentativeWindow.composeCRTPatch_cost line 165