The Navier–Stokes scaling onto the unit cylinder

The scaling step of cor:interior:nonanalytic: for 0 < R ≤ 1 the parabolic rescaling u ↦ R u(R ·, R² ·), π ↦ R² π(R ·, R² ·), f ↦ R³ f(R ·, R² ·) about the origin carries a suitable weak solution on the unit cylinder Q, restricted to B(R) × (-R², 0), to a suitable weak solution on Q, and it preserves the energy class eq:interior:energy:class, the axisymmetric core eq:interior:core, and regularity at the origin eq:interior:regular.

theorem CIV.rescaleVelocity_origin_apply (R : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.rescaleVelocity R (0, 0) u z = R • u (R • z.1, R ^ 2 * z.2)

The rescaled velocity about the origin, read on the components of a space-time point.

theorem CIV.rescaleForce_origin_apply (R : ℝ) (f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.rescaleForce R (0, 0) f z = R ^ 3 • f (R • z.1, R ^ 2 * z.2)

The rescaled force about the origin, read on the components of a space-time point.

theorem CIV.rescaledSpace_vec3Ball_self {R : ℝ} (hR0 : 0 < R) : CKN.rescaledSpace R 0 (CKN.Foundation.Parabolic.vec3Ball 0 R) = CKN.Foundation.Parabolic.vec3Ball 0 1

The spatial dilation by R > 0 pulls the ball B(R) back to the unit ball.

theorem CIV.rescaledTime_Ioo_self {R : ℝ} (hR0 : 0 < R) : CKN.rescaledTime R 0 (Set.Ioo (-R ^ 2) 0) = Set.Ioo (-1) 0

The time dilation by R² > 0 pulls (-R², 0) back to (-1, 0).

theorem CIV.isSuitableWeakSolution_rescale_unitCylinder {q R : ℝ} (hR0 : 0 < R) (hR1 : R ≤ 1) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hsol : CKN.IsSuitableWeakSolution (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0) q u Du p f) : CKN.IsSuitableWeakSolution (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0) q (CKN.rescaleVelocity R (0, 0) u) (CKN.rescaleGradient R (0, 0) Du) (CKN.rescalePressure R (0, 0) p) (CKN.rescaleForce R (0, 0) f)

The scaling step of cor:interior:nonanalytic for the solution class: a suitable weak solution on Q, restricted to B(R) × (-R², 0) and rescaled by R, is a suitable weak solution on Q.

theorem CIV.axisymmetricCore_rescale {R : ℝ} (hR0 : 0 < R) (hR1 : R ≤ 1) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hcore : ∀ t ∈ Set.Ioo (-1) 0, ∃ ρ ∈ Set.Ioo 0 1, IsAxisymmetricOn u (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 ρ) {t})) (t : ℝ) : t ∈ Set.Ioo (-1) 0 → ∃ ρ ∈ Set.Ioo 0 1, IsAxisymmetricOn (CKN.rescaleVelocity R (0, 0) u) (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 ρ) {t})

The rescaled velocity about the origin inherits an axisymmetric core eq:interior:core.

theorem CIV.boundedNearOrigin_of_rescale {R : ℝ} (hR0 : 0 < R) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (h : BoundedNearOrigin (CKN.rescaleVelocity R (0, 0) u)) : BoundedNearOrigin u

Regularity at the origin eq:interior:regular descends from the rescaled velocity.

theorem CIV.rescaleForce_eq_zero_of_vanishing {R R' δ' : ℝ} (hR0 : 0 < R) (hRR' : R ≤ R') (hRδ : R ^ 2 ≤ δ') {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hvan : ∀ z ∈ CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 R') (Set.Ioo (-δ') 0), f z = 0) (z : CKN.Foundation.Parabolic.ParabolicPoint) : z ∈ unitCylinder → CKN.rescaleForce R (0, 0) f z = 0

If the force vanishes on B(R') × (-δ', 0), the force rescaled by R ≤ R' with R² ≤ δ' vanishes on the unit cylinder.

theorem CIV.globalEnergyClass_rescale {R : ℝ} (hR0 : 0 < R) (hR1 : R ≤ 1) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (henergy : GlobalEnergyClass u Du p) : GlobalEnergyClass (CKN.rescaleVelocity R (0, 0) u) (CKN.rescaleGradient R (0, 0) Du) (CKN.rescalePressure R (0, 0) p)

The rescaling by 0 < R ≤ 1 about the origin preserves the energy class eq:interior:energy:class on the unit cylinder.