symmetric_second_diff_limit_hypothesis

formal source

 856namespace Constructive
 857
 858/-- Hypothesis: Symmetric second difference limit. -/
 859def symmetric_second_diff_limit_hypothesis (H : ℝ → ℝ) (t : ℝ) : Prop :=
 860  H 0 = 1 → Continuous H → (∀ t u, H (t+u) + H (t-u) = 2 * H t * H u) →
 861    HasDerivAt (deriv H) 1 0 → Filter.Tendsto (fun u => (H (t+u) + H (t-u) - 2 * H t) / u^2) (nhds 0) (nhds (H t))
 862
 863end Constructive
 864
 865/-! ## Aczél's Theorem and the ODE Derivation
 866
 867These results close the five regularity hypothesis gaps in `washburn_uniqueness`.
 868After adding the single Aczél axiom, all five `_hypothesis` defs become provable, and
 869a clean no-hypothesis version of the uniqueness theorem follows.
 870-/
 871
 872/-- The `dAlembert_continuous_implies_smooth_hypothesis` holds for every H,
 873    as a direct consequence of the Aczél axiom. -/
 874theorem dAlembert_smooth_of_aczel [AczelSmoothnessPackage] (H : ℝ → ℝ) :
 875    dAlembert_continuous_implies_smooth_hypothesis H :=
 876  fun h_one h_cont h_dAlembert => aczel_dAlembert_smooth H h_one h_cont h_dAlembert
 877
 878/-- **Theorem (ODE Derivation, universal coefficient)**: If H is C∞ and
 879satisfies d'Alembert, then `H''(t) = H''(0) * H(t)` everywhere.
 880
 881This is the unnormalized form of `dAlembert_to_ODE_theorem`. -/
 882theorem dAlembert_to_ODE_general_theorem (H : ℝ → ℝ)
 883    (h_smooth : ContDiff ℝ ⊤ H)
 884    (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u) :
 885    ∀ t, deriv (deriv H) t = deriv (deriv H) 0 * H t := by
 886  have hCDiff2 : ContDiff ℝ 2 H := h_smooth.of_le le_top
 887  have hDiff : Differentiable ℝ H :=
 888    hCDiff2.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
 889  have hCDiff1_H' : ContDiff ℝ 1 (deriv H) := by