theorem
proved
rk4Step_eq_self_of_zero
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.RGTransport on GitHub at line 160.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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 :
184 |k1 + 2 * k2 + 2 * k3 + k4| ≤ |k1| + 2 * |k2| + 2 * |k3| + |k4| := by
185 nlinarith [hsum1, hsum2, hsum3, h2k2, h2k3]
186 have hsumM : |k1 + 2 * k2 + 2 * k3 + k4| ≤ 6 * M := by
187 nlinarith [hsum, hk1, hk2, hk3, hk4]
188 calc
189 |rk4Increment h k1 k2 k3 k4|
190 = |h / 6| * |k1 + 2 * k2 + 2 * k3 + k4| := by