OAI/Analysis/PlanarPacking/InterpolationError.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Error bounds for cardinal interpolation

Norm bounds for the inverse interpolation operator control the distance from the finite coefficient families to the exact solution.

  1. def OAI.SharpPlanar.exactList line 13
  2. def OAI.SharpPlanar.coefficientError line 14
  3. lemma OAI.SharpPlanar.coefficientError_equation line 15
  4. lemma OAI.SharpPlanar.pair_error_plus line 22
  5. lemma OAI.SharpPlanar.pair_error_minus line 29
  6. lemma OAI.SharpPlanar.discard_add_bound line 36
  7. lemma OAI.SharpPlanar.discard_sub_bound line 42
  8. lemma OAI.SharpPlanar.pair_error_estimate line 48