theorem proved term proof

`dAlembert_to_ODE_of_contDiff`

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

formal statement (Lean)

 120theorem dAlembert_to_ODE_of_contDiff
 121    (Hf : ℝ → ℝ)
 122    (h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u)
 123    (h_diff : ContDiff ℝ 2 Hf)
 124    (h_deriv2_zero : deriv (deriv Hf) 0 = 1) :
 125    ∀ t, deriv (deriv Hf) t = Hf t := by

proof body

Term-mode proof.

 126  intro t
 127  have h_rel := dAlembert_second_deriv_at_zero_of_contDiff Hf h_dAlembert h_diff t
 128  rw [h_deriv2_zero] at h_rel
 129  linarith
 130
 131/-- Bridge from an explicit `ContDiff ℝ 2` hypothesis to the legacy ODE hypothesis. -/

used by (2)

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

dAlembert_cosh_solution_of_contDiff in IndisputableMonolith.Cost.ContDiffReduction decl_use
dAlembert_to_ODE_hypothesis_of_contDiff in IndisputableMonolith.Cost.ContDiffReduction decl_use

depends on (3)

Lean names referenced from this declaration's body.

dAlembert_second_deriv_at_zero_of_contDiff in IndisputableMonolith.Cost.ContDiffReduction decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
Bridge in IndisputableMonolith.RecogSpec.Core decl_use