theorem
proved
cosh_dAlembert_smooth
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Cost.FunctionalEquation on GitHub at line 540.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
537 deriv (deriv H) 0 = 1 → ∀ t, deriv (deriv H) t = H t
538
539/-- cosh satisfies the d'Alembert smoothness hypothesis. -/
540theorem cosh_dAlembert_smooth : dAlembert_continuous_implies_smooth_hypothesis Real.cosh := by
541 intro _ _ _
542 exact Real.contDiff_cosh
543
544/-- cosh satisfies the d'Alembert to ODE hypothesis. -/
545theorem cosh_dAlembert_to_ODE : dAlembert_to_ODE_hypothesis Real.cosh := by
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 : ℝ → ℝ)