Scaling Swirl Vertical Exponent

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

theorem CIV.swirlVerticalAnisoResidualExponent_ge {h : ℝ} (hh : 0 ≤ h) (b : ℕ) : -(2 * h) ≤ 2 * h * (↑b - 1)

The swirl/vertical anisotropic residual exponent 2*h*(b-1) is bounded below by -(2*h) when h ≥ 0 and b is a natural number, with equality exactly at b = 0.

theorem CIV.rpow_swirlVerticalAnisoResidualExponent_le {R : ℝ} (hR0 : 0 < R) (hR1 : R ≤ 1) {h : ℝ} (hh : 0 ≤ h) (b : ℕ) : R ^ (2 * h * (↑b - 1)) ≤ R ^ (-(2 * h))

When 0 < R ≤ 1 and h ≥ 0, the swirl/vertical anisotropic residual exponent is at least -(2*h), so R^(2*h*(b-1)) ≤ R^(-(2*h)).

theorem CIV.rpow_scaled_eq_swirlVerticalAnisoResidual {C h t R : ℝ} (ht : t < 0) (hR0 : 0 < R) (a b : ℕ) : R ^ (1 + a + b) * C * (-(R ^ 2 * t)) ^ (-(1 / 2) - h - ↑a / 2 - (1 / 2 - h) * ↑b) = R ^ (2 * h * (↑b - 1)) * C * (-t) ^ (-(1 / 2) - h - ↑a / 2 - (1 / 2 - h) * ↑b)

Under the parabolic rescaling u → R u(R·, R²·), the swirl/vertical anisotropic bound of eq:aniso:bounds (the angular-mean form is eq:interior:mean:bounds), C * (-t)^(-1/2 - h - a/2 - (1/2-h)*b), is rescaled to R^(1+a+b) * C * (-(R²*t))^(-1/2 - h - a/2 - (1/2-h)*b), and the residual power of R is exactly (1+a+b) + 2*(-1/2 - h - a/2 - (1/2-h)*b) = 2*h*(b-1).

theorem CIV.rpow_scaled_le_of_swirlVerticalAnisoBound {C h t R : ℝ} (hC : 0 ≤ C) (hh0 : 0 ≤ h) (ht : t < 0) (hR0 : 0 < R) (hR1 : R ≤ 1) (a b : ℕ) : R ^ (1 + a + b) * C * (-(R ^ 2 * t)) ^ (-(1 / 2) - h - ↑a / 2 - (1 / 2 - h) * ↑b) ≤ R ^ (-(2 * h)) * C * (-t) ^ (-(1 / 2) - h - ↑a / 2 - (1 / 2 - h) * ↑b)

Under the parabolic rescaling u → R u(R·, R²·) with 0 < R ≤ 1, the swirl/vertical conjunct of eq:aniso:bounds survives only with the enlarged constant R^(-(2*h)) * C: the residual power of R is 2*h*(b-1) ≥ -(2*h), so the rescaling factor is at most R^(-(2*h)), which is ≥ 1. Contrast the radial conjunct, whose residual power 2*h*b is nonnegative and whose constant is therefore unchanged.

theorem CIV.rpow_scaled_eq_of_swirlVerticalAnisoBound_of_b_eq_zero {C h t R : ℝ} (ht : t < 0) (hR0 : 0 < R) (a : ℕ) : R ^ (1 + a) * C * (-(R ^ 2 * t)) ^ (-(1 / 2) - h - ↑a / 2) = R ^ (-(2 * h)) * C * (-t) ^ (-(1 / 2) - h - ↑a / 2)

The constant R^(-(2*h)) is attained: at b = 0 the rescaled swirl/vertical bound equals R^(-(2*h)) * C * (-t)^(-1/2 - h - a/2) exactly, so no smaller constant works. This is the asymmetry with the radial conjunct, whose constant is unchanged.

theorem CIV.exists_swirlVerticalAnisoBound_rescaled {C h : ℝ} (hC : 0 ≤ C) (hh0 : 0 ≤ h) {R : ℝ} (hR0 : 0 < R) (hR1 : R ≤ 1) : ∃ (C' : ℝ), 0 ≤ C' ∧ C' = R ^ (-(2 * h)) * C ∧ ∀ t < 0, ∀ (a b : ℕ), R ^ (1 + a + b) * C * (-(R ^ 2 * t)) ^ (-(1 / 2) - h - ↑a / 2 - (1 / 2 - h) * ↑b) ≤ C' * (-t) ^ (-(1 / 2) - h - ↑a / 2 - (1 / 2 - h) * ↑b)

For any C ≥ 0, 0 ≤ h, and 0 < R ≤ 1, the rescaled swirl/vertical anisotropic bound holds with the constant C' = R^(-(2*h)) * C, for all t < 0 and all a, b : ℕ. Unlike the radial conjunct, the constant is genuinely enlarged.