UniformDefectBound

formal source

 107/-! ## Defect Bounds and Regularity -/
 108
 109/-- Uniform bound on the defect over a symmetric interval. -/
 110def UniformDefectBound (H : ℝ → ℝ) (T ε : ℝ) : Prop :=
 111  ∀ t u : ℝ, |t| ≤ T → |u| ≤ T → |dAlembertDefect H t u| ≤ ε
 112
 113/-- The standard hypothesis bundle for the stability theorem. -/
 114structure StabilityHypotheses (H : ℝ → ℝ) (T : ℝ) where
 115  /-- H is at least C³ on [-T, T] -/
 116  smooth : ContDiff ℝ 3 H
 117  /-- H is even: H(-t) = H(t) -/
 118  even : Function.Even H
 119  /-- H(0) = 1 -/
 120  normalized : H 0 = 1
 121  /-- H''(0) = a > 0 -/
 122  curvature : ℝ
 123  curvature_pos : 0 < curvature
 124  curvature_eq : deriv (deriv H) 0 = curvature
 125  /-- T > 0 -/
 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