structure
definition
StabilityBounds
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.DAlembert.Stability on GitHub at line 129.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
126 T_pos : 0 < T
127
128/-- Bound constants for the stability estimate. -/
129structure StabilityBounds (H : ℝ → ℝ) (T : ℝ) where
130 /-- Uniform defect bound: |Δ_H(t,u)| ≤ ε for |t|,|u| ≤ T -/
131 ε : ℝ
132 ε_nonneg : 0 ≤ ε
133 defect_bound : UniformDefectBound H T ε
134 /-- Uniform bound on |H|: |H(t)| ≤ B for |t| ≤ T -/
135 B : ℝ
136 B_pos : 0 < B
137 H_bound : ∀ t : ℝ, |t| ≤ T → |H t| ≤ B
138 /-- Uniform bound on |H'''|: |H'''(t)| ≤ K for |t| ≤ T -/
139 K : ℝ
140 K_nonneg : 0 ≤ K
141 H'''_bound : ∀ t : ℝ, |t| ≤ T → |iteratedDeriv 3 H t| ≤ K
142
143/-! ## The δ(h) Error Function -/
144
145/-- The error bound function δ(h) from Theorem 7.1.
146
147For step size h > 0, the local error is controlled by:
148 δ(h) := ε/h² + (1+B)·K·h/3
149
150where:
151- ε is the defect bound
152- B is the H-bound
153- K is the H'''-bound -/
154noncomputable def δ_error (ε B K h : ℝ) : ℝ :=
155 ε / h^2 + (1 + B) * K * h / 3
156
157/-- δ(h) is positive when ε, K, h > 0 and B ≥ 0. -/
158lemma δ_error_pos (ε B K h : ℝ) (hε : 0 < ε) (hB : 0 ≤ B) (hK : 0 ≤ K) (hh : 0 < h) :
159 0 < δ_error ε B K h := by