Swirl Source

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

theorem CIV.mul_zoomS_eq_circulation (lam h zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : (ℝ × ℝ) × ℝ) : p.1.1 * zoomS lam h zc u p = lam ^ (2 * h) * circulation u (zoomPoint lam h zc p)

The identity p.1.1 * zoomS = lam^(2h) * circulation at the zoomed point (eq:aniso:zoom:finite:source:a). Unfolding the definitions of zoomS and circulation and the meridional plane component gives p.1.1 * lam * lam^(2h) * u_θ = lam^(2h) * (lam * p.1.1 * u_θ).

theorem CIV.abs_mul_zoomS_le_of_circulation {lam h zc CΓ : ℝ} (hlam : 0 < lam) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {p : (ℝ × ℝ) × ℝ} (hΓ : |circulation u (zoomPoint lam h zc p)| ≤ CΓ) : |p.1.1 * zoomS lam h zc u p| ≤ CΓ * lam ^ (2 * h)

The absolute value of p.1.1 * zoomS is bounded by CΓ * lam^(2h) whenever the circulation at the zoomed point is bounded by CΓ (eq:aniso:zoom:finite:source:a).

theorem CIV.zoomPoint_segment_mem (lam h zc : ℝ) (hlam : 0 < lam) {p : (ℝ × ℝ) × ℝ} (hp : zoomPoint lam h zc p ∈ unitCylinder) {s : ℝ} (hs : s ∈ Set.Icc 0 1) : zoomPoint lam h zc ((s * p.1.1, p.1.2), p.2) ∈ unitCylinder

The zoom point of a convex combination of p with s ∈ [0,1] stays in the unit cylinder whenever p does: the radial segment to the axis stays in the preimage because the unit ball is convex, as in the remark preceding eq:aniso:zoom:finite:bound. The time coordinate is unchanged, and the spatial ball condition follows from `(lam * s * p.1.1)^2 ≤ (lam

• p.1.1)^2since0 ≤ s ≤ 1`.

theorem CIV.zoomPoint_slice_mem (lam h zc : ℝ) (hlam : 0 < lam) {p : (ℝ × ℝ) × ℝ} (hp : zoomPoint lam h zc p ∈ unitCylinder) (hR : p.1.1 ≠ 0) {s : ℝ} (hs : s ∈ Set.uIcc 0 p.1.1) : zoomPoint lam h zc ((s, p.1.2), p.2) ∈ unitCylinder

The radial-segment form of zoomPoint_segment_mem: every s between 0 and the radius p.1.1 — in either order — has its zoom point in the unit cylinder whenever p does. The scaling parameter handed to zoomPoint_segment_mem is s / p.1.1, which lies in [0, 1] exactly when s lies in uIcc 0 p.1.1.

theorem CIV.zoomS_axis (lam h zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (haxi : IsAxisymmetricOn u unitCylinder) {Z τ : ℝ} (hp : zoomPoint lam h zc ((0, Z), τ) ∈ unitCylinder) : zoomS lam h zc u ((0, Z), τ) = 0

The swirl of an axisymmetric field vanishes on the axis of the zoom-in map, as u_θ does (the remark preceding eq:aniso:zoom:finite:source:b). At p.1.1 = 0 the zoom point lies on the rotation axis, so apply_axis_one forces u_θ = 0 and hence zoomS = 0.

theorem CIV.abs_zoomS_div_le {C h lam zc : ℝ} (hlam : 0 < lam) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (haxi : IsAxisymmetricOn u unitCylinder) {p : (ℝ × ℝ) × ℝ} (hp : zoomPoint lam h zc p ∈ unitCylinder) (hR : p.1.1 ≠ 0) (hτ : p.2 ≤ -1) (hC : 0 ≤ C) (hh : 0 ≤ h) : |zoomS lam h zc u p / p.1.1| ≤ C

Bound on |zoomS / r| away from the axis (eq:aniso:zoom:finite:source:b). Applies abs_div_le_of_deriv_bound to g(r) = zoomS(..., (r, Z), τ) on the interval between 0 and p.1.1. The derivative bound comes from abs_dr_zoomW_add_abs_dr_zoomS_le, dropping the W term and using that (-p.2)^(-1-h) ≤ 1 when -p.2 ≥ 1 and h ≥ 0.