TransformedGauss.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Actual rational transport of Gauss nodes. A common polynomial precision absorbs both the initial square-root error and the numerical flow error.

def OAI.ContinuumCoulomb.TransformedGauss.precision line 16
def OAI.ContinuumCoulomb.TransformedGauss.value line 18
theorem OAI.ContinuumCoulomb.TransformedGauss.error_budget line 23

theorem OAI.ContinuumCoulomb.TransformedGauss.error_of_endpoint_error line 38

Source documentation

This is an error-composition lemma. Its numerical-flow premise is supplied below by the proved actual manufactured Euler construction.

theorem error_of_endpoint_error (rho U C K P : ℕ) {N : ℕ} (hN : 0 < N)
    (scale S : ℚ) (sites : List (ℚ×ℚ)) (k : Registers) (b : Signs)
    (G : Position → Position) {L : ℝ≥0} (hG : LipschitzWith L G) (hL : (L:ℝ) ≤ K)
    (hendpoint : ∀ q : Triple,
      ‖position (ManufacturedEuler.approximate rho U C (precision K P) scale S sites q)-G (position q)‖ ≤
        ((precision K P:ℝ)+1)⁻¹) :
    ‖position (value rho U C K P N scale S sites k b)-
      G (gaussLatticePoint (N:ℝ)⁻¹ (RationalGaussNodes.index k b))‖ ≤ ((P:ℝ)+1)⁻¹ := by
…

Mentions: OAI.ContinuumCoulomb.Position, OAI.ContinuumCoulomb.ManufacturedEuler.approximate, OAI.ContinuumCoulomb.TransformedGauss.precision, OAI.ContinuumCoulomb.TransformedGauss.value, OAI.ContinuumCoulomb.gaussLatticePoint, OAI.ContinuumCoulomb.RationalGaussNodes.index

theorem OAI.ContinuumCoulomb.TransformedGauss.exists_uniform_constants line 60

Source documentation

The transformed-node approximation is uniform over all manufactured fields and all their actual time-one maps. U and C are fixed beforehand.

theorem exists_uniform_constants (rho : ℕ) (hrho : 0 < rho) :
    ∃ U C : ℕ, 0 < U ∧ 0 < C ∧ ∀ (K P N : ℕ), 0 < N → ∀ (scale S : ℚ),
      (1:ℝ) ≤ scale → (1:ℝ) ≤ S → ∀ (m : ℕ) (u : Fin m → ℚ×ℚ),
      Function.Injective u →
      (∀ i j, i ≠ j → 3 ≤ ‖PlanarForcingProgram.position (u i)-PlanarForcingProgram.position (u j)‖) →
      (∀ i, localizedCounterterm (GaussianFrequency.frequency rho)
        (fun j => PlanarForcingProgram.position (u j)) i ≤ scale) →
      (∀ x, |manufacturedCharge (manufacturedWellField (GaussianFrequency.frequency rho)
        scale S (fun i => PlanarForcingProgram.position (u i))) x| ≤ (rho:ℝ)/2) →
      ∀ G : Position → ℝ → Position,
      IsUnitTimeFlow (moserVelocity (rho:ℝ) (manufacturedWellField (GaussianFrequency.frequency rho)
        scale S (fun i => PlanarForcingProgram.position (u i)))) G →
…

Mentions: OAI.ContinuumCoulomb.PlanarForcingProgram.position, OAI.ContinuumCoulomb.localizedCounterterm, OAI.ContinuumCoulomb.GaussianFrequency.frequency, OAI.ContinuumCoulomb.manufacturedCharge, OAI.ContinuumCoulomb.manufacturedWellField, OAI.ContinuumCoulomb.Position, OAI.ContinuumCoulomb.IsUnitTimeFlow, OAI.ContinuumCoulomb.moserVelocity