OAI/Combinatorics/SumProduct/Alignment/RoughInterpolation01.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RoughInterpolation.Integral line 15
  2. lemma OAI.RoughInterpolation.primitive_linear line 17
  3. lemma OAI.RoughInterpolation.primitive_pow line 24
  4. theorem OAI.RoughInterpolation.integral_scaled_quotient line 31
  5. theorem OAI.RoughInterpolation.integral_of_coprime_multiples line 40
  6. lemma OAI.RoughInterpolation.integral_eval_of_lifts line 51
  7. theorem OAI.RoughInterpolation.quotient_integral_at line 57
  8. lemma OAI.RoughInterpolation.integral_rational_eval line 71
  9. lemma OAI.RoughInterpolation.lifts_iterate_derivative line 86
  10. lemma OAI.RoughInterpolation.derivative_rational_denominator line 92
  11. lemma OAI.RoughInterpolation.integral_eq_zero_of_abs_lt_one line 104
  12. theorem OAI.RoughInterpolation.derivative_eq_zero_of_small line 114
  13. theorem OAI.RoughInterpolation.exact_linear_division line 130
  14. lemma OAI.RoughInterpolation.linear_power_derivative_zero line 159
  15. lemma OAI.RoughInterpolation.integral_eq_of_near line 171
  16. def OAI.ExactInterpolation.uniformConstant line 195
  17. def OAI.ExactInterpolation.derivativeConstant line 197
  18. lemma OAI.ExactInterpolation.derivativeConstant_pos line 201
  19. lemma OAI.ExactInterpolation.derivative_sum_le line 208
  20. lemma OAI.ExactInterpolation.quotient_degree line 219
  21. theorem OAI.ExactInterpolation.quantitative_exact_division line 236