ManufacturedEuler.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The literal clipped Euler iteration approximates the actual manufactured Moser flow. Its step count and denominator are fixed polynomials in the requested unary precision, uniformly over all valid input geometries.

abbrev OAI.ContinuumCoulomb.ManufacturedEuler.Environment line 16
def OAI.ContinuumCoulomb.ManufacturedEuler.evaluate line 18
def OAI.ContinuumCoulomb.ManufacturedEuler.approximate line 21
theorem OAI.ContinuumCoulomb.ManufacturedEuler.approximation_error line 27

theorem OAI.ContinuumCoulomb.ManufacturedEuler.exists_uniform_constants line 102

Source documentation

Fixed program constants work simultaneously for every valid manufactured field. No oracle for a potential, derivative, or flow value is used.

theorem exists_uniform_constants (rho : ℕ) (hrho : 0 < rho) :
    ∃ U C : ℕ, 0 < U ∧ 0 < C ∧ ∀ (P : ℕ) (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