393private theorem dAlembert_contDiff_top (H : ℝ → ℝ) 394 (h_one : H 0 = 1) (h_cont : Continuous H) 395 (h_dAl : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) : 396 ContDiff ℝ ⊤ H := by
proof body
Term-mode proof.
397 rcases dAlembert_classification H h_one h_cont h_dAl with h | ⟨α, h⟩ | ⟨α, h⟩ 398 · rw [show H = fun _ => (1 : ℝ) from funext h] 399 exact contDiff_const 400 · rw [show H = fun t => Real.cosh (α * t) from funext h] 401 exact Real.contDiff_cosh.comp (contDiff_const.mul contDiff_id) 402 · rw [show H = fun t => Real.cos (α * t) from funext h] 403 exact Real.contDiff_cos.comp (contDiff_const.mul contDiff_id) 404 405/-! ## Instance -/ 406 407instance : AczelSmoothnessPackage where 408 smooth_of_dAlembert H h_one h_cont h_dAl := dAlembert_contDiff_top H h_one h_cont h_dAl 409 410end 411 412end FunctionalEquation 413end Cost 414end IndisputableMonolith
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.