pith. machine review for the scientific record. sign in
lemma proved tactic proof

defect_even_in_t

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  66lemma defect_even_in_t (H : ℝ → ℝ) (hEven : Function.Even H) (t u : ℝ) :
  67    dAlembertDefect H t u = dAlembertDefect H (-t) u := by

proof body

Tactic-mode proof.

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

depends on (8)

Lean names referenced from this declaration's body.