The meridional segment through the axis

The continuity statements for u_r / r and for ω_θ / r across the axis are all proved the same way: the quotient at (x₁, 0, x₃) is an average of a radial derivative along the segment s ↦ (s x₁, 0, x₃), s ∈ [0, 1], which stays inside the unit ball. This module collects the elementary facts about that segment and about the clamp s ↦ max 0 (min s 1) used to extend the segment parameter to all of ℝ, so that the several quotient modules share one copy.

theorem CIV.mem_unitCylinder_meridional (x₃ : ℝ) (hx : |x₃| < 1) (t : ℝ) (ht : t ∈ Set.Ioo (-1) 0) : (meridional 0 x₃, t) ∈ unitCylinder

A point of the axis at height |x₃| < 1 lies in the unit cylinder at every time of (-1, 0).

theorem CIV.meridional_apply_zero (x₁ x₃ : ℝ) : meridional x₁ x₃ 0 = x₁

The first coordinate of a meridional point is its axis distance.

theorem CIV.meridional_eq (a x₃ : ℝ) : meridional a x₃ = a • CKN.basisVec 0 + x₃ • CKN.basisVec 2

The meridional point (a, 0, x₃) written in the standard basis.

theorem CIV.hasDerivAt_meridional_scale (x₁ x₃ s : ℝ) : HasDerivAt (fun (s : ℝ) => meridional (s * x₁) x₃) (x₁ • CKN.basisVec 0) s

The segment s ↦ (s x₁, 0, x₃) from the axis to (x₁, 0, x₃) is affine in s, with constant velocity x₁ e₁.

theorem CIV.meridional_scale_mem_vec3Ball {x₁ x₃ s : ℝ} (hx : x₁ ^ 2 + x₃ ^ 2 < 1) (hs : |s| ≤ 1) : meridional (s * x₁) x₃ ∈ CKN.Foundation.Parabolic.vec3Ball 0 1

The segment from the axis to a meridional point of the open unit ball stays in the open unit ball, and so does its extension by any parameter of size at most one.

theorem CIV.clamp_mem_Icc (s : ℝ) : max 0 (min s 1) ∈ Set.Icc 0 1

The clamp max 0 (min s 1) of a real number lands in [0, 1].

theorem CIV.abs_clamp_le_one (s : ℝ) : |max 0 (min s 1)| ≤ 1

The clamp of a real number has size at most one.

theorem CIV.clamp_eq_self {s : ℝ} (hs : s ∈ Set.Icc 0 1) : max 0 (min s 1) = s

The clamp fixes every point of [0, 1].