defect_symmetric

formal source

  94  ring
  95
  96/-- The defect is symmetric: Δ(t,u) = Δ(u,t) when H is even. -/
  97lemma defect_symmetric (H : ℝ → ℝ) (hEven : Function.Even H) (t u : ℝ) :
  98    dAlembertDefect H t u = dAlembertDefect H u t := by
  99  simp only [dAlembertDefect]
 100  have h1 : t + u = u + t := add_comm t u
 101  have h2 : H (t - u) = H (u - t) := by
 102    calc H (t - u) = H (-(u - t)) := by ring_nf
 103      _ = H (u - t) := hEven _
 104  rw [h1, h2]
 105  ring
 106
 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