Rescaling

Supporting results for the Constantin–Ignatova–Vicol axisymmetric regularity theorem.

noncomputable def CIV.zoomPoint (lam h zc : ℝ) (p : (ℝ × ℝ) × ℝ) : CKN.Foundation.Parabolic.ParabolicPoint

The zoom-in map of eq:aniso:zoom:finite:variables.

Equations

• CIV.zoomPoint lam h zc p = (CIV.meridional (lam * p.1.1) (zc + lam ^ (1 - 2 * h) * p.1.2), lam ^ 2 * p.2)

noncomputable def CIV.zoomV (lam h zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : (ℝ × ℝ) × ℝ) : ℝ

V_n, the radial component of the rescaled velocity, of eq:aniso:zoom:fields.

Equations

• CIV.zoomV lam h zc u p = lam * u (CIV.zoomPoint lam h zc p) 0

noncomputable def CIV.zoomW (lam h zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : (ℝ × ℝ) × ℝ) : ℝ

W_n, the vertical component of the rescaled velocity, of eq:aniso:zoom:fields.

Equations

• CIV.zoomW lam h zc u p = lam * lam ^ (2 * h) * u (CIV.zoomPoint lam h zc p) 2

noncomputable def CIV.zoomS (lam h zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : (ℝ × ℝ) × ℝ) : ℝ

S_n, the swirl component of the rescaled velocity, of eq:aniso:zoom:fields.

Equations

• CIV.zoomS lam h zc u p = lam * lam ^ (2 * h) * u (CIV.zoomPoint lam h zc p) 1

theorem CIV.zoomPoint_mem_unitCylinder_iff (lam h zc : ℝ) (p : (ℝ × ℝ) × ℝ) : zoomPoint lam h zc p ∈ unitCylinder ↔ (lam * p.1.1) ^ 2 + (zc + lam ^ (1 - 2 * h) * p.1.2) ^ 2 < 1 ∧ lam ^ 2 * p.2 ∈ Set.Ioo (-1) 0

The time sign is lam ^ 2 * p.2 with p.2 = τ < 0, so the selected time τ = -1 maps to t = -lam². This is the paper's convention and the corrected sign; do not change it.

theorem CIV.continuous_zoomPoint (lam h zc : ℝ) : Continuous fun (p : (ℝ × ℝ) × ℝ) => zoomPoint lam h zc p

zoomPoint is affine in p (with lam, h, zc fixed), hence continuous. ParabolicPoint carries the parabolic metric rather than the product one (design note R2), so the statement is given on the explicit product carrier Vec3 × ℝ: naming the codomain Y := Vec3 × ℝ fixes the TopologicalSpace instance to the product one before zoomPoint's own ParabolicPoint-typed body is elaborated, since a bare type ascription on the body is defeq-transparent and would leave the ParabolicPoint instance in place.

theorem CIV.contDiff_zoomPoint (lam h zc : ℝ) : ContDiff ℝ ↑⊤ fun (p : (ℝ × ℝ) × ℝ) => zoomPoint lam h zc p

zoomPoint is affine, hence smooth. ParabolicPoint carries the parabolic metric rather than the product one (design note R2), so the statement is given on the explicit product carrier Vec3 × ℝ, naming the codomain F := Vec3 × ℝ for the same reason as continuous_zoomPoint.