pith. machine review for the scientific record. sign in
def definition def or abbrev

dAlembert_continuous_implies_smooth_hypothesis

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)

 525def dAlembert_continuous_implies_smooth_hypothesis (H : ℝ → ℝ) : Prop :=

proof body

Definition body.

 526  H 0 = 1 → Continuous H → (∀ t u, H (t+u) + H (t-u) = 2 * H t * H u) → ContDiff ℝ ⊤ H
 527
 528/-- **d'Alembert to ODE derivation.**
 529
 530    If H satisfies the d'Alembert equation and is smooth, then H'' = H.
 531
 532    Proof sketch: Differentiate H(t+u) + H(t-u) = 2H(t)H(u) twice with respect to u,
 533    then set u = 0 to get H''(t) = H''(0) · H(t). With calibration H''(0) = 1, this
 534    gives H''(t) = H(t). -/

used by (16)

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

depends on (11)

Lean names referenced from this declaration's body.