OAI/Combinatorics/SumProduct/Alignment/ConstantCoefficient01.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RoughSamplingWeights.jointAffine line 28
  2. theorem OAI.RoughSamplingWeights.jointAffine_degree line 33
  3. theorem OAI.RoughSamplingWeights.rescaled_discrepancy line 47
  4. theorem OAI.RoughSamplingWeights.fixed_period_preserves_scales line 63
  5. def OAI.RoughScales.Smooth line 85
  6. def OAI.RoughScales.Rough line 87
  7. lemma OAI.RoughScales.rough_iff_coprime line 90
  8. lemma OAI.RoughScales.smooth_of_abs_le line 102
  9. lemma OAI.RoughScales.coprime_smooth_rough line 107
  10. lemma OAI.RoughScales.denominator_dvd_of_integral_multiple line 115
  11. lemma OAI.RoughScales.coefficients_smooth line 124
  12. lemma OAI.RoughScales.derivative_error_bound line 135
  13. lemma OAI.RoughScales.inverse_ratio_tendsto line 160
  14. lemma OAI.RoughSamplingWeights.period_coprime_of_rough line 180
  15. theorem OAI.RoughSamplingWeights.source_rescaled_discrepancy line 191
  16. lemma OAI.ConstantCoefficientRationalization.fwdDiff_cast line 218
  17. lemma OAI.ConstantCoefficientRationalization.fwdDiff_eval_nat line 226
  18. lemma OAI.ConstantCoefficientRationalization.fwdDiff_sub line 235
  19. lemma OAI.ConstantCoefficientRationalization.fwdDiff_constant line 245
  20. lemma OAI.ConstantCoefficientRationalization.abs_fwdDiff_le line 257
  21. theorem OAI.ConstantCoefficientRationalization.floor_difference_zero line 277
  22. lemma OAI.ConstantCoefficientRationalization.higher_difference_zero line 308
  23. def OAI.ConstantCoefficientRationalization.newtonPolynomial line 324
  24. lemma OAI.ConstantCoefficientRationalization.newtonPolynomial_eval line 328
  25. lemma OAI.ConstantCoefficientRationalization.newtonPolynomial_degree line 337
  26. theorem OAI.ConstantCoefficientRationalization.newtonPolynomial_agrees line 345
  27. theorem OAI.ConstantCoefficientRationalization.newtonPolynomial_factorial_denominator line 368
  28. theorem OAI.ConstantCoefficientRationalization.constant_coefficient_rationalization line 386
  29. theorem OAI.ConstantCoefficientRationalization.finite_van_der_waerden line 414
  30. lemma OAI.ConstantCoefficientRationalization.fractional_cell_bound line 459
  31. theorem OAI.ConstantCoefficientRationalization.constant_coefficient_after_thinning line 477