OAI/Algebra/AlgebraicObstruction/TaylorRemainder.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.monomialFactor line 15
  2. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.coeff_monomialFactor line 21
  3. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.monomial_factorization line 35
  4. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.monomialFactor_vanishes line 45
  5. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.constantCoeff_killCompl line 64
  6. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.Jet.killCompl line 69
  7. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.killCompl_subst line 77
  8. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.dropExponent line 93
  9. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.embed_dropExponent line 96
  10. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.coeff_eq_zero_of_killCompl line 104
  11. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.single_le_exponent line 110
  12. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.no_delta_coeff line 113
  13. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.no_two_delta_coeff line 122
  14. abbrev OAI.BoundaryOnly.FormalObstruction.FormalCorrection.Extended line 152
  15. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.baseArguments line 154
  16. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.shiftedArguments line 157
  17. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.baseArguments_centered line 161
  18. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.shiftedArguments_centered line 164
  19. abbrev OAI.BoundaryOnly.FormalObstruction.FormalCorrection.dropDelta line 168
  20. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.dropDelta_baseArguments line 171
  21. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.dropDelta_X line 175
  22. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.dropDelta_shiftedArguments line 182
  23. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.dropDelta_subst_base line 190
  24. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.dropDelta_subst_shifted line 195
  25. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.pderiv_delta_subst_base line 200
  26. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.pderiv_delta_subst_shifted line 205
  27. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.universalDifference line 211
  28. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.universalRemainder line 214
  29. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.dropDelta_difference line 217
  30. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.dropDelta_remainder line 221
  31. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.dropDelta_pderiv_remainder line 226
  32. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.universalDifference_vanishes line 232
  33. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.universalRemainder_vanishes line 237
  34. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.exists_taylor_remainder line 249
  35. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.exists_first_remainder line 288
  36. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.exists_gradient_remainder line 307