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

dAlembert_cosh_solution_of_contDiff

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)

 170theorem dAlembert_cosh_solution_of_contDiff
 171    (Hf : ℝ → ℝ)
 172    (h_one : Hf 0 = 1)
 173    (h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u)
 174    (h_diff : ContDiff ℝ 2 Hf)
 175    (h_deriv2_zero : deriv (deriv Hf) 0 = 1) :
 176    ∀ t, Hf t = Real.cosh t := by

proof body

Term-mode proof.

 177  have h_ode : ∀ t, deriv (deriv Hf) t = Hf t :=
 178    dAlembert_to_ODE_of_contDiff Hf h_dAlembert h_diff h_deriv2_zero
 179  have h_even : Function.Even Hf := dAlembert_even Hf h_one h_dAlembert
 180  have h_diff0 : DifferentiableAt ℝ Hf 0 :=
 181    (contDiffTwo_differentiable h_diff).differentiableAt
 182  have h_deriv_zero : deriv Hf 0 = 0 :=
 183    even_deriv_at_zero Hf h_even h_diff0
 184  exact ode_cosh_uniqueness_contdiff Hf h_diff h_ode h_one h_deriv_zero
 185
 186/-- Sharpened T5 surface:
 187normalization, the composition law, calibration, and `C²` regularity of `H = G + 1`
 188already force the canonical reciprocal cost. Reciprocal symmetry is derived, not assumed. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (30)

Lean names referenced from this declaration's body.