OAI/Computability/RationalHitting/TaylorComputation.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RationalHitting.StackLanguage.range_sum_fin line 8
  2. lemma OAI.RationalHitting.StackLanguage.finEquiv_val line 12
  3. lemma OAI.RationalHitting.StackLanguage.finEquiv_symm_val line 18
  4. lemma OAI.RationalHitting.StackLanguage.finEquiv_cast line 23
  5. lemma OAI.RationalHitting.StackLanguage.range_sum_zmod line 28
  6. lemma OAI.RationalHitting.StackLanguage.zmod_val_sub line 38
  7. lemma OAI.RationalHitting.StackLanguage.coordinate_vals line 42
  8. def OAI.RationalHitting.StackLanguage.Runtime.taylorTerm line 57
  9. def OAI.RationalHitting.StackLanguage.Runtime.taylor line 61
  10. def OAI.RationalHitting.StackLanguage.Runtime.padded line 64
  11. lemma OAI.RationalHitting.StackLanguage.Runtime.taylor_eq line 67
  12. lemma OAI.RationalHitting.StackLanguage.Runtime.padded_eq line 75
  13. abbrev OAI.RationalHitting.StackLanguage.Runtime.TaylorArgs line 79
  14. theorem OAI.RationalHitting.StackLanguage.Runtime.taylorTerm_poly line 81
  15. theorem OAI.RationalHitting.StackLanguage.Runtime.taylor_poly line 90
  16. theorem OAI.RationalHitting.StackLanguage.Runtime.padded_poly line 94
  17. abbrev OAI.RationalHitting.StackLanguage.Params line 108
  18. abbrev OAI.RationalHitting.StackLanguage.Params.n line 110
  19. abbrev OAI.RationalHitting.StackLanguage.Params.N line 111
  20. abbrev OAI.RationalHitting.StackLanguage.Params.m line 112
  21. abbrev OAI.RationalHitting.StackLanguage.Params.q line 113
  22. abbrev OAI.RationalHitting.StackLanguage.Params.H line 114
  23. def OAI.RationalHitting.StackLanguage.Params.of line 116
  24. def OAI.RationalHitting.StackLanguage.Params.BB line 122
  25. def OAI.RationalHitting.StackLanguage.Params.DD line 123
  26. def OAI.RationalHitting.StackLanguage.Params.threshold line 124
  27. def OAI.RationalHitting.StackLanguage.Params.EE line 125
  28. def OAI.RationalHitting.StackLanguage.Params.MM line 126
  29. def OAI.RationalHitting.StackLanguage.Params.NN line 127
  30. def OAI.RationalHitting.StackLanguage.Params.HH line 128
  31. def OAI.RationalHitting.StackLanguage.Params.QQ line 129
  32. theorem OAI.RationalHitting.StackLanguage.Poly.paramB line 132
  33. theorem OAI.RationalHitting.StackLanguage.Poly.paramDelta line 135
  34. theorem OAI.RationalHitting.StackLanguage.Poly.paramThreshold line 138
  35. theorem OAI.RationalHitting.StackLanguage.Poly.paramExponent line 141
  36. theorem OAI.RationalHitting.StackLanguage.Poly.paramM line 142
  37. theorem OAI.RationalHitting.StackLanguage.Poly.paramN line 148
  38. theorem OAI.RationalHitting.StackLanguage.Poly.paramH line 151
  39. theorem OAI.RationalHitting.StackLanguage.Poly.paramDegree line 154
  40. theorem OAI.RationalHitting.StackLanguage.Poly.params line 160