deriv_phi_eq
plain-language theorem explainer
The lemma shows that the integral antiderivative of a continuous real-valued function H recovers H exactly upon differentiation. Analysts working on regularity bootstrap for d'Alembert equations cite this step when lifting continuity to C^1 in the Aczél classification. The proof is a one-line term wrapper that applies functional extensionality to the pointwise hasDerivAt property of the integral.
Claim. Let $Φ(t) := ∫_0^t H(s) ds$. If $H:ℝ→ℝ$ is continuous, then $dΦ/dt = H(t)$.
background
The Aczél theorem module proves that every continuous solution of the d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u) with H(0)=1 is C^∞, yielding the classification into cosh, cos, or constant cases. Phi is the antiderivative defined by integrating H from 0 to t. Upstream, H is the shifted cost H(x) = J(x) + 1 = ½(x + x^{-1}), which converts the recognition composition law into the standard d'Alembert equation. The phi_hasDerivAt result supplies the local differentiability of the integral under continuity.
proof idea
This is a one-line term-mode wrapper. It uses funext to reduce to each t, then applies the hasDerivAt property of Phi at t and extracts the derivative value.
why it matters
The lemma advances the integration bootstrap in the Aczél smoothness argument, supplying the C^1 step that feeds phi_contDiff_succ and the subsequent induction to C^∞. It supports elimination of the former H_AczelClassification hypothesis in the cost algebra. The result aligns with the module's strategy of deriving the ODE H'' = c H from infinite differentiability plus the functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.