OAI/MathematicalPhysics/ContinuumCoulomb/Programs/MoserDifferenceProgram.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Literal polynomial integer arithmetic for the fixed finite-difference precision and rational step of the manufactured field evaluator.

  1. opaque OAI.ContinuumCoulomb.MoserDifferenceBudget.nextSquareProgram line 12
  2. opaque OAI.ContinuumCoulomb.MoserDifferenceBudget.nextCubeProgram line 16
  3. opaque OAI.ContinuumCoulomb.MoserDifferenceBudget.precisionScaleData line 22

    Source documentation

    A fixed integer bounds the finite-difference precision independently of the input instance.

    noncomputable opaque precisionScaleData : {n : ℕ // n = 16384*guard^2} := ⟨16384*guard^2,rfl⟩

    Mentions: OAI.ContinuumCoulomb.MoserDifferenceBudget.guard

  4. def OAI.ContinuumCoulomb.MoserDifferenceBudget.precisionScale line 23
  5. theorem OAI.ContinuumCoulomb.MoserDifferenceBudget.precisionScale_eq line 25
  6. opaque OAI.ContinuumCoulomb.MoserDifferenceBudget.precisionProgram line 27
  7. opaque OAI.ContinuumCoulomb.MoserDifferenceBudget.stepDenominatorProgram line 35
  8. opaque OAI.ContinuumCoulomb.MoserDifferenceBudget.stepProgram line 41