dAlembert_double

formal source

 103  have h := h_dAlembert 0 u
 104  simpa [h_one, zero_add, sub_eq_add_neg, two_mul] using h
 105
 106lemma dAlembert_double
 107  (H : ℝ → ℝ)
 108  (h_one : H 0 = 1)
 109  (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u) (t : ℝ) :
 110  H (2 * t) = 2 * (H t)^2 - 1 := by
 111  have h := h_dAlembert t t
 112  have h' : H (t + t) = 2 * (H t)^2 - 1 := by
 113    -- H(2t) + H(0) = 2 H(t)^2
 114    have h0 : H (t + t) + 1 = 2 * H t * H t := by
 115      simpa [h_one] using h
 116    have h1 : H (t + t) = 2 * H t * H t - 1 := by
 117      linarith
 118    simpa [pow_two, mul_assoc] using h1
 119  simpa [two_mul] using h'
 120
 121lemma dAlembert_product
 122  (H : ℝ → ℝ)
 123  (h_one : H 0 = 1)
 124  (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u) :
 125  ∀ t u, H (t+u) * H (t-u) = (H t)^2 + (H u)^2 - 1 := by
 126  intro t u
 127  have h := h_dAlembert (t + u) (t - u)
 128  have h' : H (2 * t) + H (2 * u) = 2 * H (t + u) * H (t - u) := by
 129    -- (t+u)+(t-u)=2t and (t+u)-(t-u)=2u
 130    simpa [two_mul, sub_eq_add_neg, add_assoc, add_left_comm, add_comm] using h
 131  have h2t : H (2 * t) = 2 * (H t)^2 - 1 := dAlembert_double H h_one h_dAlembert t
 132  have h2u : H (2 * u) = 2 * (H u)^2 - 1 := dAlembert_double H h_one h_dAlembert u
 133  have h'' : 2 * H (t + u) * H (t - u) = (2 * (H t)^2 - 1) + (2 * (H u)^2 - 1) := by
 134    calc
 135      2 * H (t + u) * H (t - u) = H (2 * t) + H (2 * u) := by linarith [h']
 136      _ = (2 * (H t)^2 - 1) + (2 * (H u)^2 - 1) := by simp [h2t, h2u]