OAI/Combinatorics/SumProduct/Alignment/RoughRational01.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RoughPolynomialDegree.coordinate line 26
  2. lemma OAI.RoughPolynomialDegree.power line 29
  3. lemma OAI.RoughPolynomialDegree.finite_sum line 34
  4. lemma OAI.RoughPolynomialDegree.finite_prod line 44
  5. lemma OAI.RoughPolynomialDegree.polynomial_eval line 55
  6. lemma OAI.RoughPolynomialDegree.mv_eval line 68
  7. lemma OAI.RoughPolynomialDegree.compose line 87
  8. lemma OAI.RoughPolynomialDegree.time_affine line 94
  9. lemma OAI.RoughPolynomialDegree.joint_grid line 107
  10. theorem OAI.RoughRealRationalization.real_rational_split line 154
  11. def OAI.RoughRationalKernel.rationalValue line 241
  12. def OAI.RoughRationalKernel.errorCoefficients line 243
  13. def OAI.RoughRationalKernel.errorValue line 246
  14. lemma OAI.RoughRationalKernel.error_eq line 250
  15. lemma OAI.RoughRationalKernel.rational_degree line 255
  16. lemma OAI.RoughRationalKernel.error_degree line 260
  17. lemma OAI.RoughRationalKernel.split_error_bound line 268
  18. lemma OAI.RoughRationalKernel.integer_spatial line 277
  19. lemma OAI.RoughRationalKernel.integer_spatial_on_lattice line 300
  20. theorem OAI.RoughRationalKernel.kernel_polynomial line 317