theorem
proved
tactic proof
rk4Step_deviation_le
show as:
view Lean formalization →
formal statement (Lean)
199theorem rk4Step_deviation_le (f : ℝ → ℝ) (x h M : ℝ)
200 (hk1 : |f x| ≤ M)
201 (hk2 : |f (x + (h / 2) * f x)| ≤ M)
202 (hk3 : |f (x + (h / 2) * f (x + (h / 2) * f x))| ≤ M)
203 (hk4 : |f (x + h * f (x + (h / 2) * f (x + (h / 2) * f x)))| ≤ M) :
204 |rk4Step f x h - x| ≤ |h| * M := by
proof body
Tactic-mode proof.
205 unfold rk4Step
206 set k1 : ℝ := f x
207 set k2 : ℝ := f (x + (h / 2) * k1)
208 set k3 : ℝ := f (x + (h / 2) * k2)
209 set k4 : ℝ := f (x + h * k3)
210 have hk1' : |k1| ≤ M := by simpa [k1] using hk1
211 have hk2' : |k2| ≤ M := by simpa [k1, k2] using hk2
212 have hk3' : |k3| ≤ M := by simpa [k1, k2, k3] using hk3
213 have hk4' : |k4| ≤ M := by simpa [k1, k2, k3, k4] using hk4
214 have hinc :
215 |rk4Increment h k1 k2 k3 k4| ≤ |h| * M :=
216 abs_rk4Increment_le M h k1 k2 k3 k4 hk1' hk2' hk3' hk4'
217 have hstep : |(x + rk4Increment h k1 k2 k3 k4) - x| = |rk4Increment h k1 k2 k3 k4| := by
218 ring_nf
219 simpa [hstep]
220
221/-- The integrated residue from ln-scale `lnμ₀` to `lnμ₁`.
222
223 `f(μ₀, μ₁) = (1/λ) ∫_{lnμ₀}^{lnμ₁} γ(exp(t)) dt`
224
225 This is the abstract definition; the actual computation requires the SM kernels.
226 We parameterize by an `AnomalousDimension` structure. -/