hasDerivAt_rsq_mul
plain-language theorem explainer
The lemma gives the product-rule derivative of the map t ↦ t² A'(t) at a fixed real point x, assuming A' is differentiable there with derivative A''(x). Analysts working on radial Navier-Stokes identities would cite it when carrying out integration by parts on skew forms. The proof is a one-line wrapper that first invokes the derivative of t ↦ t² and then applies the product rule for HasDerivAt.
Claim. Suppose the map A' is differentiable at x with derivative A''(x). Then the map t ↦ t² A'(t) is differentiable at x with derivative 2x A'(x) + x² A''(x).
background
The module supplies the algebraic backbone for skew/self-adjoint cancellations and harmonic-tail bookkeeping in radial Navier-Stokes profiles. Here A, A', A'' stand for a radial function and its first two derivatives; the skew identities arise from integration by parts whose cross terms must cancel exactly. The present lemma supplies the precise derivative of the quadratic weight times the first derivative, which is the local ingredient needed before any integral or boundary-term argument begins.
proof idea
The proof first obtains the derivative of t ↦ t² at x from the power-rule result for the squaring map. It then feeds this together with the given derivative of A' into the product rule for differentiable maps. Commutativity and associativity of addition and multiplication rearrange the resulting expression into the target formula.
why it matters
The result is invoked by the three downstream integral skew-identity lemmas that perform the finite-interval and half-line cancellations. It therefore realizes the 'no cross term' step described in the module documentation for the navier-dec-12-rewrite.tex arguments. Within the Recognition Science setting it contributes the local differentiation step required for the D = 3 radial analysis before tail-decay hypotheses are imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.