Scaling Radial Exponent

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

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

The radial anisotropic residual exponent 2*h*b is nonnegative when h ≥ 0 and b is a natural number.

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

When 0 < R ≤ 1 and h ≥ 0, the radial anisotropic residual exponent is nonnegative, so R^(2*h*b) ≤ 1.

theorem CIV.rpow_scaled_le_of_radialAnisoBound {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) - ↑a / 2 - (1 / 2 - h) * ↑b) ≤ C * (-t) ^ (-(1 / 2) - ↑a / 2 - (1 / 2 - h) * ↑b)

Under the parabolic rescaling u → R u(R·, R²·) with 0 < R ≤ 1, the radial anisotropic bound C * (-t)^(-1/2 - a/2 - (1/2-h)*b) is rescaled to R^(1+a+b) * C * (-(R²*t))^(-1/2 - a/2 - (1/2-h)*b). The rescaling introduces a factor R^(2*h*b) that is ≤ 1, so the original constant C still works.

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

For any C ≥ 0, 0 ≤ h, and 0 < R ≤ 1, there exists a constant C' ≥ 0 (namely C itself) such that the rescaled radial anisotropic bound holds for all t < 0 and all a, b : ℕ.