Anisotropic Bounds Rescale

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

theorem CIV.anisotropicBounds_rescale {C h R : ℝ} (hC : 0 ≤ C) (hh0 : 0 ≤ h) (hR0 : 0 < R) (hR1 : R ≤ 1) {v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hv : AnisotropicBounds C h v) : AnisotropicBounds (R ^ (-(2 * h)) * C) h (CKN.rescaleVelocity R (0, 0) v)

theorem CIV.anisotropicBounds_angularMean_rescale {C h R : ℝ} (hC : 0 ≤ C) (hh0 : 0 ≤ h) (hR0 : 0 < R) (hR1 : R ≤ 1) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : AnisotropicBounds C h (angularMean u)) : AnisotropicBounds (R ^ (-(2 * h)) * C) h (angularMean (CKN.rescaleVelocity R (0, 0) u))