optimal_h

formal source

 168Solving: h³ = 6ε/((1+B)K), so h = (6ε/((1+B)K))^{1/3}
 169
 170This gives δ(h_opt) ~ O(ε^{1/3}) -/
 171noncomputable def optimal_h (ε B K : ℝ) : ℝ :=
 172  (6 * ε / ((1 + B) * K)) ^ (1/3 : ℝ)
 173
 174/-! ## Theorem 7.1: Main Stability Estimate -/
 175
 176/-- **Theorem 7.1 (d'Alembert Stability)**
 177
 178Let H ∈ C³([-T,T]) be even with H(0) = 1, and set a := H''(0) > 0.
 179
 180Define:
 181- ε := sup_{|t|,|u| ≤ T} |Δ_H(t,u)|  (defect bound)
 182- B := sup_{|t| ≤ T} |H(t)|          (function bound)
 183- K := sup_{|t| ≤ T} |H'''(t)|       (third derivative bound)
 184- δ(h) := ε/h² + (1+B)·K·h/3        (error function)
 185
 186Then for every h with 0 < h ≤ T and every t with |t| ≤ T - h:
 187
 188  |H(t) - cosh(√a·t)| ≤ (δ(h)/a) · (cosh(√a·|t|) - 1)
 189
 190When a = 1 and δ(h) is small, this shows H ≈ cosh on compact intervals. -/
 191def StabilityEstimate (H : ℝ → ℝ) (T a : ℝ) (bounds : StabilityBounds H T) : Prop :=
 192  ∀ h : ℝ, 0 < h → h ≤ T →
 193  ∀ t : ℝ, |t| ≤ T - h →
 194  |H t - Real.cosh (Real.sqrt a * t)| ≤
 195    (δ_error bounds.ε bounds.B bounds.K h / a) * (Real.cosh (Real.sqrt a * |t|) - 1)
 196
 197/-- The ODE intermediate step: from the defect bound, we derive H'' - a·H is small.
 198
 199This is equation (7.3) in the paper:
 200  |H''(t) - a·H(t)| ≤ δ(h)  for |t| ≤ T - h -/
 201def ODEApproximation (H : ℝ → ℝ) (T a : ℝ) (bounds : StabilityBounds H T) : Prop :=