OAI/NumberTheory/Ostmann/Arithmetic/ContinuousIntervalMesh.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.continuous_interval_mesh line 12

   Source documentation

   Mesh fineness is arbitrary and has no arithmetic cost: the progression comparison uses total variation instead of counting the subintervals.

   theorem continuous_interval_mesh (u v : ℝ) (huv : u ≤ v) (w : ℝ → ℂ)
       (hw : ContinuousOn w (Set.Icc u v)) (η : ℝ) (hη : 0 < η) :
       ∃ (s : ℕ → ℝ) (N : ℕ), 0 < N ∧ Monotone s ∧ s 0 = u ∧ s N = v ∧
         ∀ j < N, ∀ y ∈ Set.Ioc (s j) (s (j + 1)), ‖w y - w (s j)‖ ≤ η := by
   …