Iterating a single spatial derivative through a constant multiple precomposed with

parabolic dilation 

Multi-index spatial derivative of a constant multiple precomposed with parabolic dilation

theorem CIV.multiPartial_const_mul_comp_scalingParabolic (c μ : ℝ) (z₀ : CKN.Foundation.Parabolic.ParabolicPoint) (g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (α : Fin 3 → ℕ) (z : CKN.Foundation.Parabolic.ParabolicPoint) : multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => c * g (CKN.scalingParabolic μ z₀ w)) α z = c * μ ^ (α 0 + α 1 + α 2) * multiPartial g α (CKN.scalingParabolic μ z₀ z)

Parabolic dilation centered at the origin

Shrinking the unit cylinder by parabolic dilation

Componentwise formula for the Navier-Stokes force rescaling

C^2 force bound survives parabolic rescaling

theorem CIV.forceC2Bounded_rescale {R : ℝ} (hR0 : 0 < R) (hR1 : R ≤ 1) {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hf : ForceC2Bounded f) : ForceC2Bounded (CKN.rescaleForce R (0, 0) f)