Upper bound on the selected sequence's scaled meridional quantity from
eq:aniso:zoom:selected, unifying CIV.neg_t_mul_meridionalQuantity_selection_eq
(the off-axis, R ≠ 0 identity) and its axis counterpart
CIV.neg_t_mul_meridionalQuantity_selection_eq_of_axis (the R = 0 case) into a
single inequality valid for every R ≥ 0. Step 2's contradiction argument needs
this bound to cover the axis-included range R ∈ [0, A].
theorem
CIV.neg_t_mul_meridionalQuantity_selection_le
{h : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hu : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder)
{t : ℝ}
(ht : t < 0)
{lam R zc : ℝ}
(hlam : 0 < lam)
(hR : 0 ≤ R)
(hlamsq : lam ^ 2 = -t)
(hp : zoomPoint lam h zc ((R, 0), -1) ∈ unitCylinder)
:
-t * (|CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 0 (meridional (lam * R) zc, t)| + |radialQuotient u (meridional (lam * R) zc, t)| + |CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 2) 2
(meridional (lam * R) zc, t)|) ≤ 2 * |dr (zoomV lam h zc u) ((R, 0), -1)| + |zoomV lam h zc u ((R, 0), -1) / R| + |dz (zoomW lam h zc u) ((R, 0), -1)|
theorem
CIV.neg_t_mul_meridionalQuantity_selection_le_sqrt
{h : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hu : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder)
{t : ℝ}
(ht : t < 0)
{R zc : ℝ}
(hR : 0 ≤ R)
(hp : zoomPoint (√(-t)) h zc ((R, 0), -1) ∈ unitCylinder)
:
-t * (|CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 0
(meridional (√(-t) * R) zc, t)| + |radialQuotient u (meridional (√(-t) * R) zc, t)| + |CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 2) 2
(meridional (√(-t) * R) zc, t)|) ≤ 2 * |dr (zoomV (√(-t)) h zc u) ((R, 0), -1)| + |zoomV (√(-t)) h zc u ((R, 0), -1) / R| + |dz (zoomW (√(-t)) h zc u) ((R, 0), -1)|
theorem
CIV.lt_of_neg_t_mul_meridionalQuantity_selection_lt
{h : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hu : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder)
{t c₀ : ℝ}
(ht : t < 0)
{lam R zc : ℝ}
(hlam : 0 < lam)
(hR : 0 ≤ R)
(hlamsq : lam ^ 2 = -t)
(hp : zoomPoint lam h zc ((R, 0), -1) ∈ unitCylinder)
(hineq :
c₀ < -t * (|CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 0
(meridional (lam * R) zc, t)| + |radialQuotient u (meridional (lam * R) zc, t)| + |CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 2) 2
(meridional (lam * R) zc, t)|))
:
theorem
CIV.lt_of_neg_t_mul_meridionalQuantity_selection_lt_sqrt
{h : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hu : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder)
{t c₀ : ℝ}
(ht : t < 0)
{R zc : ℝ}
(hR : 0 ≤ R)
(hp : zoomPoint (√(-t)) h zc ((R, 0), -1) ∈ unitCylinder)
(hineq :
c₀ < -t * (|CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 0
(meridional (√(-t) * R) zc, t)| + |radialQuotient u (meridional (√(-t) * R) zc, t)| + |CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 2) 2
(meridional (√(-t) * R) zc, t)|))
: