Commit 2026-06-01 21:42 23bafd51

refactor(Analysis/Calculus/Gradient): ungate inner_gradient lemmas (#39203) Removes superfluous differentiability hypotheses (plus UniqueDiffWithinAt for the Within versions) from the four inner_gradient[Within]_[left|right] lemmas: gradient is defined as (toDual 𝕜 F).symm (fderiv 𝕜 f x), so ⟪∇ f x, y⟫ = fderiv 𝕜 f x y holds unconditionally since both sides are zero when f is not differentiable at x.