 150  (h / 6) * (k1 + 2 * k2 + 2 * k3 + k4)
 151
 152/-- One RK4 step for `x' = f(x)` with step size `h`. -/
 153def rk4Step (f : ℝ → ℝ) (x h : ℝ) : ℝ :=
 154  let k1 := f x
 155  let k2 := f (x + (h / 2) * k1)
 156  let k3 := f (x + (h / 2) * k2)
 157  let k4 := f (x + h * k3)
 158  x + rk4Increment h k1 k2 k3 k4
 159
 160theorem rk4Step_eq_self_of_zero (f : ℝ → ℝ)
 161    (hzero : ∀ y, f y = 0) (x h : ℝ) :
 162    rk4Step f x h = x := by
 163  simp [rk4Step, rk4Increment, hzero]
 164
 165/-- Algebraic enclosure: if each RK4 stage is bounded by `M`, then one-step
 166deviation is bounded by `|h|*M`. -/
 167theorem abs_rk4Increment_le (M h k1 k2 k3 k4 : ℝ)
 168    (hk1 : |k1| ≤ M) (hk2 : |k2| ≤ M)
 169    (hk3 : |k3| ≤ M) (hk4 : |k4| ≤ M) :
 170    |rk4Increment h k1 k2 k3 k4| ≤ |h| * M := by
 171  have hsum1 : |k1 + 2 * k2 + 2 * k3 + k4| ≤ |k1| + |2 * k2 + 2 * k3 + k4| := by
 172    simpa [Real.norm_eq_abs, add_assoc] using
 173      (norm_add_le k1 (2 * k2 + 2 * k3 + k4))
 174  have hsum2 : |2 * k2 + 2 * k3 + k4| ≤ |2 * k2| + |2 * k3 + k4| := by
 175    simpa [Real.norm_eq_abs, add_assoc] using
 176      (norm_add_le (2 * k2) (2 * k3 + k4))
 177  have hsum3 : |2 * k3 + k4| ≤ |2 * k3| + |k4| := by
 178    simpa [Real.norm_eq_abs] using (norm_add_le (2 * k3) k4)
 179  have h2k2 : |2 * k2| = 2 * |k2| := by
 180    norm_num [abs_mul]
 181  have h2k3 : |2 * k3| = 2 * |k3| := by
 182    norm_num [abs_mul]
 183  have hsum :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.