phi_hasDerivAt
plain-language theorem explainer
The lemma states that for any continuous H : ℝ → ℝ the antiderivative Phi(H)(t) := ∫ from 0 to t of H(s) ds is differentiable at every t with derivative exactly H(t). Analysts working on functional equations cite it as the initial bootstrap step that converts continuity into differentiability inside the proof of Aczél's smoothness theorem. The proof is a direct one-line wrapper around Mathlib's intervalIntegral.integral_hasDerivAt_right using the supplied continuity hypotheses.
Claim. Let $H : ℝ → ℝ$ be continuous. Define the antiderivative $Φ(t) := ∫_0^t H(s) ds$. Then $Φ$ is differentiable at every real $t$ and $Φ'(t) = H(t)$.
background
The module establishes Aczél's smoothness theorem: every continuous solution $H$ of the d'Alembert equation $H(t+u) + H(t-u) = 2 H(t) H(u)$ with $H(0)=1$ is real analytic. The argument opens with an integration bootstrap that introduces the antiderivative $Φ(H)(t) := ∫_0^t H(s) ds$. This lemma supplies the fundamental theorem of calculus step that recovers the original $H$ as the derivative of $Φ$. Upstream, $H$ is obtained from the Recognition cost function by the shift $H = J + 1$, which converts the Recognition Composition Law into the classical d'Alembert equation.
proof idea
The proof is a one-line wrapper that applies intervalIntegral.integral_hasDerivAt_right. It passes the interval integrability of $H$ on [0,t], the strong measurability coming from continuity, and the continuity-at-t filter to obtain HasDerivAt (Phi H) (H t) t.
why it matters
This lemma starts the differentiability chain that produces deriv_phi_eq, phi_differentiable, exists_integral_ne_zero and the representation_formula used to derive the second-order ODE. It is invoked by the corresponding results in AczelTheorem and directly implements the first step of the integration bootstrap described in the module documentation for Aczél's 1966 theorem. The result sits inside the larger Recognition Science program that derives analyticity of the cost function from the functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.