dAlembertDefect

formal source

  54
  55When Δ_H ≡ 0, H is an exact d'Alembert solution.
  56When |Δ_H| ≤ ε, H is an approximate solution. -/
  57def dAlembertDefect (H : ℝ → ℝ) (t u : ℝ) : ℝ :=
  58  H (t + u) + H (t - u) - 2 * H t * H u
  59
  60/-- The defect is zero iff H satisfies the d'Alembert equation at (t, u). -/
  61lemma defect_zero_iff_dAlembert (H : ℝ → ℝ) (t u : ℝ) :
  62    dAlembertDefect H t u = 0 ↔ H (t + u) + H (t - u) = 2 * H t * H u := by
  63  simp [dAlembertDefect, sub_eq_zero]
  64
  65/-- For even H with H(0) = 1, the defect is symmetric in t ↔ -t. -/
  66lemma defect_even_in_t (H : ℝ → ℝ) (hEven : Function.Even H) (t u : ℝ) :
  67    dAlembertDefect H t u = dAlembertDefect H (-t) u := by
  68  simp only [dAlembertDefect]
  69  -- By evenness: H(-x) = H x, so H x = H(-x) by symmetry
  70  have h1 : H (t + u) = H (-t - u) := by
  71    calc H (t + u) = H (-(- (t + u))) := by ring_nf
  72      _ = H (-(-t - u)) := by ring_nf
  73      _ = H (-t - u) := hEven _
  74  have h2 : H (t - u) = H (-t + u) := by
  75    calc H (t - u) = H (-(-(t - u))) := by ring_nf
  76      _ = H (-(-t + u)) := by ring_nf
  77      _ = H (-t + u) := hEven _
  78  have h3 : H t = H (-t) := (hEven t).symm
  79  rw [h1, h2, h3]
  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)