RationalGaussNodes.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Rational initial nodes for the tensor Gauss rule on mesh 1/N. The only irrational constant is evaluated by the existing dyadic square-root program; the error bound is uniform over the entire integer lattice.

abbrev OAI.ContinuumCoulomb.RationalGaussNodes.Signs line 18
def OAI.ContinuumCoulomb.RationalGaussNodes.abscissa line 20
def OAI.ContinuumCoulomb.RationalGaussNodes.signed line 21
def OAI.ContinuumCoulomb.RationalGaussNodes.index line 22
def OAI.ContinuumCoulomb.RationalGaussNodes.value line 24
theorem OAI.ContinuumCoulomb.RationalGaussNodes.abscissa_error line 28
theorem OAI.ContinuumCoulomb.RationalGaussNodes.signed_error line 40
theorem OAI.ContinuumCoulomb.RationalGaussNodes.coordinate_error line 49
theorem OAI.ContinuumCoulomb.RationalGaussNodes.approximation_error line 62
theorem OAI.ContinuumCoulomb.RationalGaussNodes.transported_error line 89
Source documentation
The initial-node error and the rational ODE solver error add after transport by the actual common Lipschitz map.
```
theorem transported_error (G : Position → Position) {K : ℝ≥0} (hG : LipschitzWith K G)
    (P : ℕ) {N : ℕ} (hN : 0 < N) (k : Registers) (b : Signs)
    (out : Triple) {δ : ℝ}
    (he : ‖position out-G (position (value P N k b))‖ ≤ δ) :
    ‖position out-G (gaussLatticePoint (N:ℝ)⁻¹ (index k b))‖ ≤
      δ+(K:ℝ)*((P:ℝ)+1)⁻¹ := by
…
```
Mentions: OAI.ContinuumCoulomb.Position, OAI.ContinuumCoulomb.RationalGaussNodes.Signs, OAI.ContinuumCoulomb.RationalGaussNodes.value, OAI.ContinuumCoulomb.gaussLatticePoint, OAI.ContinuumCoulomb.RationalGaussNodes.index