defect_even_in_t

formal source

  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)
  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. -/