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

dAlembert_cosh_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)

 549theorem dAlembert_cosh_solution
 550    (H : ℝ → ℝ)
 551    (h_one : H 0 = 1)
 552    (h_cont : Continuous H)
 553    (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u)
 554    (h_deriv2_zero : deriv (deriv H) 0 = 1)
 555    (h_smooth_hyp : dAlembert_continuous_implies_smooth_hypothesis H)
 556    (h_ode_hyp : dAlembert_to_ODE_hypothesis H)
 557    (h_cont_hyp : ode_regularity_continuous_hypothesis H)
 558    (h_diff_hyp : ode_regularity_differentiable_hypothesis H)
 559    (h_bootstrap_hyp : ode_linear_regularity_bootstrap_hypothesis H) :
 560    ∀ t, H t = Real.cosh t := by

proof body

Tactic-mode proof.

 561  have h_ode : ∀ t, deriv (deriv H) t = H t := h_ode_hyp h_one h_cont h_dAlembert h_deriv2_zero
 562  have h_even : Function.Even H := dAlembert_even H h_one h_dAlembert
 563  have h_deriv_zero : deriv H 0 = 0 := by
 564    have h_smooth := h_smooth_hyp h_one h_cont h_dAlembert
 565    have h_diff : DifferentiableAt ℝ H 0 := h_smooth.differentiable (by decide : (⊤ : WithTop ℕ∞) ≠ 0) |>.differentiableAt
 566    exact even_deriv_at_zero H h_even h_diff
 567  exact ode_cosh_uniqueness H h_ode h_one h_deriv_zero h_cont_hyp h_diff_hyp h_bootstrap_hyp
 568

used by (8)

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.