rk4Step_deviation_le

formal source

 196    _ = |h| * M := by ring
 197
 198/-- RK4 one-step enclosure bound for function evaluations at the four RK stages. -/
 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
 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. -/
 227def integratedResidue (γ : AnomalousDimension) (f : Fermion) (lnμ₀ lnμ₁ : ℝ) : ℝ :=
 228  (1 / lambda) * ∫ t in Set.Icc lnμ₀ lnμ₁, γ.gamma f (Real.exp t)
 229