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

dAlembert_cosh_solution_aczel

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)

1053theorem dAlembert_cosh_solution_aczel
1054    [AczelSmoothnessPackage]
1055    (H : ℝ → ℝ)
1056    (h_one : H 0 = 1)
1057    (h_cont : Continuous H)
1058    (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u)
1059    (h_d2_zero : deriv (deriv H) 0 = 1) :
1060    ∀ t, H t = Real.cosh t := by

proof body

Term-mode proof.

1061  have h_smooth : ContDiff ℝ ⊤ H := aczel_dAlembert_smooth H h_one h_cont h_dAlembert
1062  have hDiff : Differentiable ℝ H :=
1063    (h_smooth.of_le le_top : ContDiff ℝ 1 H).differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
1064  have h_even : Function.Even H := dAlembert_even H h_one h_dAlembert
1065  have h_H'0 : deriv H 0 = 0 := even_deriv_at_zero H h_even hDiff.differentiableAt
1066  have h_ode : ∀ t, deriv (deriv H) t = H t :=
1067    dAlembert_to_ODE_theorem H h_smooth h_dAlembert h_d2_zero
1068  have h_C2 : ContDiff ℝ 2 H := h_smooth.of_le le_top
1069  exact ode_cosh_uniqueness_contdiff H h_C2 h_ode h_one h_H'0
1070
1071/-- **Theorem (Washburn, clean form)**: The J-cost function is the unique
1072    reciprocal cost satisfying the RCL, normalization, calibration, and continuity.
1073
1074    This version uses the global Aczél axiom internally and requires NO regularity
1075    hypothesis parameters from the caller. -/

used by (8)

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

depends on (22)

Lean names referenced from this declaration's body.