Algebra

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

theorem CIV.sq_div_le_of_abs_mul_le {S R D ε : ℝ} (hε : 0 < ε) (hR : ε ≤ R) (h : |R * S| ≤ D) : (S / R) ^ 2 ≤ D ^ 2 / ε ^ 4

If |R * S| ≤ D with ε > 0 and ε ≤ R, then (S / R)^2 ≤ D^2 / ε^4.

theorem CIV.sq_div_le_of_abs_le_mul {S R C : ℝ} (hR : 0 < R) (h : |S| ≤ C * R) : (S / R) ^ 2 ≤ C ^ 2

If |S| ≤ C * R with R > 0, then (S / R)^2 ≤ C^2.

theorem CIV.neg_rpow_le_one_of_le_neg_one {τ e : ℝ} (hτ : τ ≤ -1) (he : e ≤ 0) : (-τ) ^ e ≤ 1

For τ ≤ -1 and e ≤ 0, we have (-τ)^e ≤ 1.

theorem CIV.finite_axis_bound_le {δ τ h C : ℝ} (hC : 0 ≤ C) (hδ : 0 ≤ δ) (hδ1 : δ ≤ 1) (hτ : τ ≤ -1) (hh : 0 < h ∧ h < 1 / 2) : C * (δ ^ 2 * (-τ) ^ (-(3 / 2) + h) + (-τ) ^ (-(3 / 2) - h)) ≤ 2 * C

Finite axis bound: for C ≥ 0, 0 ≤ δ ≤ 1, τ ≤ -1, 0 < h < 1/2, C * (δ^2 * (-τ)^(-3/2 + h) + (-τ)^(-3/2 - h)) ≤ 2 * C.

theorem CIV.neg_t_mul_rpow_neg_half {t : ℝ} (ht : t < 0) : -t * (-t) ^ (-(1 / 2)) = (-t) ^ (1 / 2)

(-t) * (-t)^(-1/2) = (-t)^(1/2) for t < 0.

theorem CIV.neg_t_mul_rpow_neg_one_add {t h : ℝ} (ht : t < 0) : -t * (-t) ^ (-1 + h) = (-t) ^ h

(-t) * (-t)^(-1 + h) = (-t)^h for t < 0.