Time derivatives of rescaled profiles #
For a profile Ψ : E → F, a fixed point x : E, and real exponents a and b, the expression
s^(-a) Ψ(s^b x) is differentiable at each s > 0 where Ψ is differentiable at y = s^b x,
and its derivative is s^(-(a + 1)) (-a Ψ(y) + b DΨ(y) y). The derivative is again of the same
form with a new profile, so iterated time derivatives of self-similar expressions, such as the
derivatives of the heat kernel under parabolic scaling, can be computed by induction.
theorem
TauCeti.hasDerivAt_rpow_smul_comp_rpow_smul
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{Ψ : E → F}
(a b : ℝ)
(x : E)
{s : ℝ}
(hs : 0 < s)
(hΨ : DifferentiableAt ℝ Ψ (s ^ b • x))
:
The time derivative of a rescaled profile:
∂ₛ (s^(-a) Ψ(s^b x)) = s^(-(a + 1)) (-a Ψ(y) + b DΨ(y) y) with y = s^b x, provided Ψ is
differentiable at y.