lemma
proved
dAlembert_even
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Cost.FunctionalEquation on GitHub at line 97.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
94 rw [h1] at h2
95 linarith
96
97lemma dAlembert_even
98 (H : ℝ → ℝ)
99 (h_one : H 0 = 1)
100 (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u) :
101 Function.Even H := by
102 intro u
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)