defect_even_in_u

formal source

  80  ring
  81
  82/-- The defect is symmetric in u ↔ -u. -/
  83lemma defect_even_in_u (H : ℝ → ℝ) (hEven : Function.Even H) (t u : ℝ) :
  84    dAlembertDefect H t u = dAlembertDefect H t (-u) := by
  85  simp only [dAlembertDefect]
  86  have h1 : H u = H (-u) := (hEven u).symm
  87  -- Goal: H(t+u) + H(t-u) - 2*H(t)*H(u) = H(t-(-u)) + H(t+(-u)) - 2*H(t)*H(-u)
  88  -- Note: t - (-u) = t + u, t + (-u) = t - u
  89  -- So RHS = H(t+u) + H(t-u) - 2*H(t)*H(-u)
  90  -- With h1: H(u) = H(-u), the equation becomes LHS = LHS
  91  have heq1 : t - (-u) = t + u := by ring
  92  have heq2 : t + (-u) = t - u := by ring
  93  rw [heq1, heq2, ← h1]
  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. -/