The endpoint argument on the meridional half-plane

Let V W : ℝ × ℝ → ℝ be the radial and axial components of a divergence-free axisymmetric meridional field on the closed half-plane {R ≥ 0}, of class C¹ on the open half-plane {R > 0} and with V bounded there. Assume the two structural identities

• ∂_R V + V / R + ∂_Z W = 0 on {R > 0} (the divergence identity), and
• ∂_R W = 0 on {R > 0}.

Then V vanishes identically and both ∂_R V and ∂_Z W vanish identically. The three steps are the three theorems endpoint_axial_const, endpoint_radial_eq and endpoint_dz_axial_eq_zero:

• ∂_R W = 0 on the connected half-line {R > 0} makes W (R, Z) independent of R, hence ∂_Z W (R, Z) = ∂_Z W (1, Z) is a function c Z of Z alone;
• the divergence identity then reads ∂_R (R V) = −R · c Z, so R V (R, Z) + (R² / 2) · c Z is constant in R; boundedness of V forces that constant to be 0, i.e. V (R, Z) = −(R / 2) · c Z;
• boundedness of V on the whole half-line now forces c Z = 0, by eq_zero_of_abs_mul_le_of_nonneg.

Derivatives are taken in the form produced by CIV.exists_subseq_tendstoUniformlyOn_c1: a Fréchet derivative DV p : (ℝ × ℝ) →L[ℝ] ℝ at p : ℝ × ℝ, whose radial and axial partial derivatives are DV p (1, 0) and DV p (0, 1).

The second half of the file transfers the conclusion to a C¹-convergent sequence: if DV n → DV⁰ uniformly on a set on which the limiting radial derivative vanishes, then ∂_R V n → 0 uniformly there, and the radial quotients V n / R converge to 0 uniformly on a segment [0, A] × {Z} of the closed half-plane, by the mean value theorem applied to R ↦ V n (R, Z) on [0, R].

Elementary one-variable input

Reading partial derivatives off a Fréchet derivative

theorem CIV.hasDerivAt_radial_of_hasFDerivAt {f : ℝ × ℝ → ℝ} {L : ℝ × ℝ →L[ℝ] ℝ} {R Z : ℝ} (hf : HasFDerivAt f L (R, Z)) : HasDerivAt (fun (r : ℝ) => f (r, Z)) (L (1, 0)) R

The radial slice of a function with a Fréchet derivative at (R, Z) has derivative L (1, 0) at R.

theorem CIV.hasDerivAt_axial_of_hasFDerivAt {f : ℝ × ℝ → ℝ} {L : ℝ × ℝ →L[ℝ] ℝ} {R Z : ℝ} (hf : HasFDerivAt f L (R, Z)) : HasDerivAt (fun (z : ℝ) => f (R, z)) (L (0, 1)) Z

The axial slice of a function with a Fréchet derivative at (R, Z) has derivative L (0, 1) at Z.

theorem CIV.dr_eq_of_hasFDerivAt (phi : (ℝ × ℝ) × ℝ → ℝ) (t : ℝ) {L : ℝ × ℝ →L[ℝ] ℝ} {R Z : ℝ} (hphi : HasFDerivAt (fun (p : ℝ × ℝ) => phi (p, t)) L (R, Z)) : dr phi ((R, Z), t) = L (1, 0)

The repository's dr of a space-time field, at a fixed time, read off the Fréchet derivative of the corresponding time slice.

theorem CIV.dz_eq_of_hasFDerivAt (phi : (ℝ × ℝ) × ℝ → ℝ) (t : ℝ) {L : ℝ × ℝ →L[ℝ] ℝ} {R Z : ℝ} (hphi : HasFDerivAt (fun (p : ℝ × ℝ) => phi (p, t)) L (R, Z)) : dz phi ((R, Z), t) = L (0, 1)

The repository's dz of a space-time field, at a fixed time, read off the Fréchet derivative of the corresponding time slice.

Step (a): the axial component does not depend on the radius

theorem CIV.endpoint_axial_const (W : ℝ × ℝ → ℝ) (DW : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ) (hW : ∀ (p : ℝ × ℝ), 0 < p.1 → HasFDerivAt W (DW p) p) (hWr : ∀ (p : ℝ × ℝ), 0 < p.1 → (DW p) (1, 0) = 0) (R Z : ℝ) (hR : 0 < R) : W (R, Z) = W (1, Z)

If ∂_R W = 0 on the open half-plane, then W (R, Z) = W (1, Z) for every R > 0.

theorem CIV.endpoint_dz_axial_const (W : ℝ × ℝ → ℝ) (DW : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ) (hW : ∀ (p : ℝ × ℝ), 0 < p.1 → HasFDerivAt W (DW p) p) (hWr : ∀ (p : ℝ × ℝ), 0 < p.1 → (DW p) (1, 0) = 0) (R Z : ℝ) (hR : 0 < R) : (DW (R, Z)) (0, 1) = (DW (1, Z)) (0, 1)

If ∂_R W = 0 on the open half-plane, then ∂_Z W (R, Z) = ∂_Z W (1, Z) for every R > 0: the axial derivative of W is a function of Z alone.

Step (b): the radial component is linear in the radius

theorem CIV.endpoint_radial_eq (V W : ℝ × ℝ → ℝ) (DV DW : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ) (M : ℝ) (hV : ∀ (p : ℝ × ℝ), 0 < p.1 → HasFDerivAt V (DV p) p) (hW : ∀ (p : ℝ × ℝ), 0 < p.1 → HasFDerivAt W (DW p) p) (hbdd : ∀ (p : ℝ × ℝ), 0 < p.1 → |V p| ≤ M) (hdiv : ∀ (p : ℝ × ℝ), 0 < p.1 → (DV p) (1, 0) + V p / p.1 + (DW p) (0, 1) = 0) (hWr : ∀ (p : ℝ × ℝ), 0 < p.1 → (DW p) (1, 0) = 0) (R Z : ℝ) (hR : 0 < R) : V (R, Z) = -(R / 2) * (DW (1, Z)) (0, 1)

The divergence identity integrates from the axis: with c Z := ∂_Z W (1, Z) one has V (R, Z) = −(R / 2) · c Z for every R > 0. The integration constant is killed by the boundedness of V, which makes R · V (R, Z) tend to 0 as R → 0⁺.

Step (c): boundedness forces the endpoint field to vanish

theorem CIV.endpoint_dz_axial_eq_zero (V W : ℝ × ℝ → ℝ) (DV DW : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ) (M : ℝ) (hV : ∀ (p : ℝ × ℝ), 0 < p.1 → HasFDerivAt V (DV p) p) (hW : ∀ (p : ℝ × ℝ), 0 < p.1 → HasFDerivAt W (DW p) p) (hbdd : ∀ (p : ℝ × ℝ), 0 < p.1 → |V p| ≤ M) (hdiv : ∀ (p : ℝ × ℝ), 0 < p.1 → (DV p) (1, 0) + V p / p.1 + (DW p) (0, 1) = 0) (hWr : ∀ (p : ℝ × ℝ), 0 < p.1 → (DW p) (1, 0) = 0) (Z : ℝ) : (DW (1, Z)) (0, 1) = 0

Boundedness of V on the whole half-plane forces the Z-derivative of W to vanish.

theorem CIV.endpoint_radial_eq_zero (V W : ℝ × ℝ → ℝ) (DV DW : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ) (M : ℝ) (hV : ∀ (p : ℝ × ℝ), 0 < p.1 → HasFDerivAt V (DV p) p) (hW : ∀ (p : ℝ × ℝ), 0 < p.1 → HasFDerivAt W (DW p) p) (hbdd : ∀ (p : ℝ × ℝ), 0 < p.1 → |V p| ≤ M) (hdiv : ∀ (p : ℝ × ℝ), 0 < p.1 → (DV p) (1, 0) + V p / p.1 + (DW p) (0, 1) = 0) (hWr : ∀ (p : ℝ × ℝ), 0 < p.1 → (DW p) (1, 0) = 0) (p : ℝ × ℝ) (hp : 0 < p.1) : V p = 0

The radial component of the endpoint field vanishes on the open half-plane.

theorem CIV.endpoint_dz_axial_eq_zero_of_pos (V W : ℝ × ℝ → ℝ) (DV DW : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ) (M : ℝ) (hV : ∀ (p : ℝ × ℝ), 0 < p.1 → HasFDerivAt V (DV p) p) (hW : ∀ (p : ℝ × ℝ), 0 < p.1 → HasFDerivAt W (DW p) p) (hbdd : ∀ (p : ℝ × ℝ), 0 < p.1 → |V p| ≤ M) (hdiv : ∀ (p : ℝ × ℝ), 0 < p.1 → (DV p) (1, 0) + V p / p.1 + (DW p) (0, 1) = 0) (hWr : ∀ (p : ℝ × ℝ), 0 < p.1 → (DW p) (1, 0) = 0) (p : ℝ × ℝ) (hp : 0 < p.1) : (DW p) (0, 1) = 0

The axial derivative of the axial component vanishes on the open half-plane.

theorem CIV.endpoint_dr_radial_eq_zero (V W : ℝ × ℝ → ℝ) (DV DW : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ) (M : ℝ) (hV : ∀ (p : ℝ × ℝ), 0 < p.1 → HasFDerivAt V (DV p) p) (hW : ∀ (p : ℝ × ℝ), 0 < p.1 → HasFDerivAt W (DW p) p) (hbdd : ∀ (p : ℝ × ℝ), 0 < p.1 → |V p| ≤ M) (hdiv : ∀ (p : ℝ × ℝ), 0 < p.1 → (DV p) (1, 0) + V p / p.1 + (DW p) (0, 1) = 0) (hWr : ∀ (p : ℝ × ℝ), 0 < p.1 → (DW p) (1, 0) = 0) (p : ℝ × ℝ) (hp : 0 < p.1) : (DV p) (1, 0) = 0

The radial derivative of the radial component vanishes on the open half-plane.

theorem CIV.endpoint_fderiv_radial_eq_zero (V W : ℝ × ℝ → ℝ) (DV DW : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ) (M : ℝ) (hV : ∀ (p : ℝ × ℝ), 0 < p.1 → HasFDerivAt V (DV p) p) (hW : ∀ (p : ℝ × ℝ), 0 < p.1 → HasFDerivAt W (DW p) p) (hbdd : ∀ (p : ℝ × ℝ), 0 < p.1 → |V p| ≤ M) (hdiv : ∀ (p : ℝ × ℝ), 0 < p.1 → (DV p) (1, 0) + V p / p.1 + (DW p) (0, 1) = 0) (hWr : ∀ (p : ℝ × ℝ), 0 < p.1 → (DW p) (1, 0) = 0) (p : ℝ × ℝ) (hp : 0 < p.1) : DV p = 0

The full Fréchet derivative of the radial component vanishes on the open half-plane: V is identically zero on the open set {R > 0}.

theorem CIV.endpoint_vanishing (V W : ℝ × ℝ → ℝ) (DV DW : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ) (M : ℝ) (hV : ∀ (p : ℝ × ℝ), 0 < p.1 → HasFDerivAt V (DV p) p) (hW : ∀ (p : ℝ × ℝ), 0 < p.1 → HasFDerivAt W (DW p) p) (hbdd : ∀ (p : ℝ × ℝ), 0 < p.1 → |V p| ≤ M) (hdiv : ∀ (p : ℝ × ℝ), 0 < p.1 → (DV p) (1, 0) + V p / p.1 + (DW p) (0, 1) = 0) (hWr : ∀ (p : ℝ × ℝ), 0 < p.1 → (DW p) (1, 0) = 0) : (∀ (p : ℝ × ℝ), 0 < p.1 → V p = 0) ∧ (∀ (p : ℝ × ℝ), 0 < p.1 → (DV p) (1, 0) = 0) ∧ ∀ (p : ℝ × ℝ), 0 < p.1 → (DW p) (0, 1) = 0

The endpoint conclusion, packaged: on the open half-plane the radial component, its radial derivative, and the axial derivative of the axial component all vanish.

Transfer to a C¹-convergent sequence

theorem CIV.tendstoUniformlyOn_clm_apply (S : Set (ℝ × ℝ)) (D : ℕ → ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ) (D0 : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ) (v : ℝ × ℝ) (h : TendstoUniformlyOn D D0 Filter.atTop S) : TendstoUniformlyOn (fun (n : ℕ) (p : ℝ × ℝ) => (D n p) v) (fun (p : ℝ × ℝ) => (D0 p) v) Filter.atTop S

Uniform convergence of continuous linear maps passes to their values at a fixed vector.

theorem CIV.tendstoUniformlyOn_clm_apply_zero (S : Set (ℝ × ℝ)) (D : ℕ → ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ) (D0 : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ) (v : ℝ × ℝ) (h : TendstoUniformlyOn D D0 Filter.atTop S) (hzero : ∀ p ∈ S, (D0 p) v = 0) : TendstoUniformlyOn (fun (n : ℕ) (p : ℝ × ℝ) => (D n p) v) (fun (x : ℝ × ℝ) => 0) Filter.atTop S

If the limiting derivative annihilates v on S, the values at v converge uniformly to 0 on S.

theorem CIV.eq_zero_of_continuousOn_Icc_of_pos {f : ℝ → ℝ} {A : ℝ} (hA : 0 < A) (hcont : ContinuousOn f (Set.Icc 0 A)) (hpos : ∀ (r : ℝ), 0 < r → r ≤ A → f r = 0) (r : ℝ) : r ∈ Set.Icc 0 A → f r = 0

A continuous function on [0, A] vanishing on (0, A] vanishes on all of [0, A]: the value at the axis is recovered as a limit along A / (n + 1).

theorem CIV.tendstoUniformlyOn_radial_div (A Z : ℝ) (V : ℕ → ℝ × ℝ → ℝ) (DV : ℕ → ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ) (haxis : ∀ (n : ℕ), V n (0, Z) = 0) (hcont : ∀ (n : ℕ), ContinuousOn (fun (r : ℝ) => V n (r, Z)) (Set.Icc 0 A)) (hderiv : ∀ (n : ℕ) (p : ℝ × ℝ), 0 < p.1 → HasFDerivAt (V n) (DV n p) p) (huniform : TendstoUniformlyOn (fun (n : ℕ) (p : ℝ × ℝ) => (DV n p) (1, 0)) (fun (x : ℝ × ℝ) => 0) Filter.atTop (Set.Icc 0 A ×ˢ {Z})) : TendstoUniformlyOn (fun (n : ℕ) (p : ℝ × ℝ) => V n p / p.1) (fun (x : ℝ × ℝ) => 0) Filter.atTop (Set.Icc 0 A ×ˢ {Z})

Uniform convergence of the radial quotients V n / R to 0 on the segment [0, A] × {Z} of the closed half-plane. Each quotient is a value of the radial derivative at an intermediate radius, by the mean value theorem applied to r ↦ V n (r, Z) on [0, R]; the axis value R = 0 is covered because V n (0, Z) = 0.

theorem CIV.endpoint_tendstoUniformlyOn_triple (A Z M : ℝ) (hA : 0 < A) (V W : ℝ × ℝ → ℝ) (DV DW : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ) (Vn : ℕ → ℝ × ℝ → ℝ) (DVn DWn : ℕ → ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ) (hV : ∀ (p : ℝ × ℝ), 0 < p.1 → HasFDerivAt V (DV p) p) (hW : ∀ (p : ℝ × ℝ), 0 < p.1 → HasFDerivAt W (DW p) p) (hbdd : ∀ (p : ℝ × ℝ), 0 < p.1 → |V p| ≤ M) (hdiv : ∀ (p : ℝ × ℝ), 0 < p.1 → (DV p) (1, 0) + V p / p.1 + (DW p) (0, 1) = 0) (hWr : ∀ (p : ℝ × ℝ), 0 < p.1 → (DW p) (1, 0) = 0) (hDVcont : ContinuousOn (fun (r : ℝ) => (DV (r, Z)) (1, 0)) (Set.Icc 0 A)) (hDWcont : ContinuousOn (fun (r : ℝ) => (DW (r, Z)) (0, 1)) (Set.Icc 0 A)) (hDVconv : TendstoUniformlyOn DVn DV Filter.atTop (Set.Icc 0 A ×ˢ {Z})) (hDWconv : TendstoUniformlyOn DWn DW Filter.atTop (Set.Icc 0 A ×ˢ {Z})) (haxis : ∀ (n : ℕ), Vn n (0, Z) = 0) (hVncont : ∀ (n : ℕ), ContinuousOn (fun (r : ℝ) => Vn n (r, Z)) (Set.Icc 0 A)) (hVnderiv : ∀ (n : ℕ) (p : ℝ × ℝ), 0 < p.1 → HasFDerivAt (Vn n) (DVn n p) p) : TendstoUniformlyOn (fun (n : ℕ) (p : ℝ × ℝ) => (DVn n p) (1, 0)) (fun (x : ℝ × ℝ) => 0) Filter.atTop (Set.Icc 0 A ×ˢ {Z}) ∧ TendstoUniformlyOn (fun (n : ℕ) (p : ℝ × ℝ) => (DWn n p) (0, 1)) (fun (x : ℝ × ℝ) => 0) Filter.atTop (Set.Icc 0 A ×ˢ {Z}) ∧ TendstoUniformlyOn (fun (n : ℕ) (p : ℝ × ℝ) => Vn n p / p.1) (fun (x : ℝ × ℝ) => 0) Filter.atTop (Set.Icc 0 A ×ˢ {Z})

The endpoint conclusion of Step 2 in uniform form on the segment [0, A] × {Z} of the closed half-plane: along a sequence converging to the endpoint field in C¹, the radial derivative of the radial component, the axial derivative of the axial component, and the radial quotients all converge to 0 uniformly.