pith. machine review for the scientific record. sign in
theorem proved term proof

dAlembert_even_solution

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)

 199theorem dAlembert_even_solution
 200    (H : ℝ → ℝ)
 201    (hH0 : H 0 = 1)
 202    (hdA : ∀ t u : ℝ, H (t + u) + H (t - u) = 2 * H t * H u) :
 203    Function.Even H := by

proof body

Term-mode proof.

 204  exact dAlembert_even H hH0 hdA
 205
 206/-- **Theorem**: d'Alembert + smoothness + calibration implies cosh.
 207    Previously a hypothesis; now proved via `ode_cosh_uniqueness_contdiff`. -/

depends on (6)

Lean names referenced from this declaration's body.