OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/RationalFieldDifferences.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Coordinate differences of a rational scalar sampler approximate the actual gradient and Laplacian. The real extension below is only a proof device; the numerical expressions evaluate the sampler at rational points.

  1. theorem OAI.ContinuumCoulomb.RationalFieldDifferences.position_injective line 16
  2. def OAI.ContinuumCoulomb.RationalFieldDifferences.extend line 29
  3. theorem OAI.ContinuumCoulomb.RationalFieldDifferences.extend_at line 33
  4. theorem OAI.ContinuumCoulomb.RationalFieldDifferences.extend_error line 40
  5. def OAI.ContinuumCoulomb.RationalFieldDifferences.shift line 49
  6. theorem OAI.ContinuumCoulomb.RationalFieldDifferences.shift_position line 53
  7. def OAI.ContinuumCoulomb.RationalFieldDifferences.first line 58
  8. def OAI.ContinuumCoulomb.RationalFieldDifferences.second line 61
  9. def OAI.ContinuumCoulomb.RationalFieldDifferences.laplacian line 64
  10. theorem OAI.ContinuumCoulomb.RationalFieldDifferences.first_error line 66
  11. theorem OAI.ContinuumCoulomb.RationalFieldDifferences.second_error line 77
  12. theorem OAI.ContinuumCoulomb.RationalFieldDifferences.laplacian_error line 91