`dAlembert_cosh_solution`

proved

show as: view math explainer →

module: IndisputableMonolith.Cost.FunctionalEquation
domain: Cost
line: 549 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Cost.FunctionalEquation on GitHub at line 549.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 546  intro _ _ _ _
 547  exact cosh_second_deriv_eq
 548
 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
 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
 569theorem dAlembert_cosh_solution_of_log_curvature
 570    (H : ℝ → ℝ)
 571    (h_one : H 0 = 1)
 572    (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u)
 573    {κ : ℝ} (h_calib : HasLogCurvature H κ)
 574    (h_deriv2_zero : deriv (deriv H) 0 = 1)
 575    (h_smooth_hyp : dAlembert_continuous_implies_smooth_hypothesis H)
 576    (h_ode_hyp : dAlembert_to_ODE_hypothesis H)
 577    (h_cont_hyp : ode_regularity_continuous_hypothesis H)
 578    (h_diff_hyp : ode_regularity_differentiable_hypothesis H)
 579    (h_bootstrap_hyp : ode_linear_regularity_bootstrap_hypothesis H) :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.