Immediate consequences of the anisotropic Type II bounds #
Each of the four lemmas below extracts a pointwise estimate from
AnisotropicBounds C h u (eq:aniso:bounds) by specialising the derivative
orders (a, b) and simplifying the exponent.
theorem
CIV.abs_dz_ur_le_of_anisotropicBounds
{C h : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hb : AnisotropicBounds C h u)
{x₁ x₃ t : ℝ}
(hz : (meridional x₁ x₃, t) ∈ unitCylinder)
:
|CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 2 (meridional x₁ x₃, t)| ≤ C * (-t) ^ (-(1 / 2) - (1 / 2 - h))
∂_z u_r bound from the anisotropic Type II bounds.
Corresponds to the b = 1 term in eq:aniso:bounds.
theorem
CIV.neg_t_mul_abs_dz_ur_le
{C h : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hb : AnisotropicBounds C h u)
{x₁ x₃ t : ℝ}
(hz : (meridional x₁ x₃, t) ∈ unitCylinder)
:
-t * |CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 2 (meridional x₁ x₃, t)| ≤ C * (-t) ^ h
(-t) * |∂_z u_r| bound from the anisotropic Type II bounds, via
mul_le_mul_of_nonneg_left and the Real.rpow identity s * s ^ α = s ^ (1 + α).
theorem
CIV.abs_ur_le_of_anisotropicBounds
{C h : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hb : AnisotropicBounds C h u)
{x₁ x₃ t : ℝ}
(hz : (meridional x₁ x₃, t) ∈ unitCylinder)
:
u_r bound from the anisotropic Type II bounds at (a, b) = (0, 0).
Corresponds to the first term in eq:aniso:bounds with no derivatives.
theorem
CIV.abs_uz_add_abs_utheta_le_of_anisotropicBounds
{C h : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hb : AnisotropicBounds C h u)
{x₁ x₃ t : ℝ}
(hz : (meridional x₁ x₃, t) ∈ unitCylinder)
:
|u_z| + |u_θ| bound from the anisotropic Type II bounds at (a, b) = (0, 0).
Corresponds to the second term in eq:aniso:bounds with no derivatives.