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. -/
depends on (16)
Lean names referenced from this declaration's body.