lemma
proved
tactic proof
defect_even_in_u
show as:
view Lean formalization →
formal statement (Lean)
83lemma defect_even_in_u (H : ℝ → ℝ) (hEven : Function.Even H) (t u : ℝ) :
84 dAlembertDefect H t u = dAlembertDefect H t (-u) := by
proof body
Tactic-mode proof.
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. -/