The finite-axis case of prop:aniso:small fails

Closing argument of Step 2 of the zoom-in of Section sec:aniso:zoom (eq:aniso:zoom:finite:endpoint and the paragraph after it). In the variables eq:aniso:zoom:finite:variables the selected point (x_n, t_n) has coordinates (R, Z, τ) = (r_n/λ_n, 0, -1), and (r_n/λ_n, 0) lies in the compact set [0, A] × {0}. By eq:aniso:zoom:fields and the chain rule the selected quantity (-t_n)(|∂_r u_r| + |u_r/r| + |∂_z u_z|)(x_n, t_n) equals (|∂_R V_n| + |V_n/R| + |∂_Z W_n|)(r_n/λ_n, 0, -1), both quotients extended continuously to the axis.

The bounds eq:aniso:zoom:derivatives make V_n(·,-1) and W_n(·,-1) bounded in C² on every compact subset of the closed half-plane with one constant, so along a subsequence they converge in C¹ on those compact sets. The limits obey ∂_R V⁰ + V⁰/R + ∂_Z W⁰ = 0 and ∂_R W⁰ = 0, and the endpoint argument CIV.endpoint_tendstoUniformlyOn_triple turns this into the uniform vanishing eq:aniso:zoom:finite:endpoint on [0, A] × {0}. The selected quantity therefore tends to zero along the subsequence, contradicting its lower bound c₀ > 0 in eq:aniso:zoom:selected; that last step is CIV.false_of_finite_contradiction_data, whose nine limit and convergence hypotheses are supplied here by the extraction rather than assumed.

Everything here happens at the single time τ = -1: the compactness used is the spatial C¹ compactness CIV.exists_subseq_tendstoUniformlyOn_c1_halfPlane on a fixed time slice, and no equicontinuity in τ is claimed or needed. The two inputs that carry information from the equation — the divergence identity of eq:aniso:zoom:finite:identities and the vanishing of ∂_R W_n off the axis, which comes from Ω_n → 0 through the potential-vorticity identity CIV.zoomOmega_eq — enter as hypotheses on the sequence itself.

The factor 2 in the lower bound is the one produced by CIV.lt_of_neg_t_mul_meridionalQuantity_selection_lt, which absorbs the axis value of the quotient u_r/r into the radial derivative; it costs nothing, since all three terms are shown to vanish.

Evaluation of a convergent sequence of continuous linear maps

theorem CIV.tendsto_clm_apply_of_tendsto {F : ℕ → ℝ × ℝ →L[ℝ] ℝ} {G : ℝ × ℝ →L[ℝ] ℝ} (h : Filter.Tendsto F Filter.atTop (nhds G)) (v : ℝ × ℝ) : Filter.Tendsto (fun (n : ℕ) => (F n) v) Filter.atTop (nhds (G v))

Evaluation at a fixed vector is continuous, so a convergent sequence of continuous linear maps converges at every vector.

The endpoint data extracted from the C² bounds

theorem CIV.exists_subseq_finite_endpoint_data {A L : ℝ} (hL : 0 ≤ L) (Vseq Wseq : ℕ → ℝ × ℝ → ℝ) (hVsmooth : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (Vseq n)) (hWsmooth : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (Wseq n)) (hVbdd : ∀ (j : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ y ∈ halfPlaneRectangle j, |Vseq n y| ≤ L ∧ ‖fderiv ℝ (Vseq n) y‖ ≤ L ∧ ‖fderiv ℝ (fderiv ℝ (Vseq n)) y‖ ≤ L) (hWbdd : ∀ (j : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ y ∈ halfPlaneRectangle j, |Wseq n y| ≤ L ∧ ‖fderiv ℝ (Wseq n) y‖ ≤ L ∧ ‖fderiv ℝ (fderiv ℝ (Wseq n)) y‖ ≤ L) (hdivn : ∀ (p : ℝ × ℝ), 0 < p.1 → ∀ᶠ (n : ℕ) in Filter.atTop, (fderiv ℝ (Vseq n) p) (1, 0) + Vseq n p / p.1 + (fderiv ℝ (Wseq n) p) (0, 1) = 0) (hdWn : ∀ (p : ℝ × ℝ), 0 < p.1 → Filter.Tendsto (fun (n : ℕ) => (fderiv ℝ (Wseq n) p) (1, 0)) Filter.atTop (nhds 0)) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∃ (V : ℝ × ℝ → ℝ) (W : ℝ × ℝ → ℝ) (DV : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ) (DW : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ), (∀ (p : ℝ × ℝ), 0 < p.1 → HasFDerivAt V (DV p) p) ∧ (∀ (p : ℝ × ℝ), 0 < p.1 → HasFDerivAt W (DW p) p) ∧ (∀ (p : ℝ × ℝ), 0 < p.1 → |V p| ≤ L) ∧ (∀ (p : ℝ × ℝ), 0 < p.1 → (DV p) (1, 0) + V p / p.1 + (DW p) (0, 1) = 0) ∧ (∀ (p : ℝ × ℝ), 0 < p.1 → (DW p) (1, 0) = 0) ∧ ContinuousOn (fun (r : ℝ) => (DV (r, 0)) (1, 0)) (Set.Icc 0 A) ∧ ContinuousOn (fun (r : ℝ) => (DW (r, 0)) (0, 1)) (Set.Icc 0 A) ∧ TendstoUniformlyOn (fun (n : ℕ) => fderiv ℝ (Vseq (φ n))) DV Filter.atTop (Set.Icc 0 A ×ˢ {0}) ∧ TendstoUniformlyOn (fun (n : ℕ) => fderiv ℝ (Wseq (φ n))) DW Filter.atTop (Set.Icc 0 A ×ˢ {0})

The endpoint data of eq:aniso:zoom:finite:endpoint, extracted rather than assumed: a sequence of smooth meridional fields (V_n, W_n) on the plane which is C²-bounded by one constant L on every square [0, j+1] × [-(j+1), j+1] for all large n, satisfies the divergence identity of eq:aniso:zoom:finite:identities off the axis for all large n, and whose radial derivative ∂_R W_n tends to zero off the axis, has a subsequence along which (V_n, W_n) converges in C¹ on every such square to a pair (V⁰, W⁰) that is bounded by L on the open half-plane, divergence free there, and independent of R in its axial component.

The nine conclusions are exactly the nine hypotheses hV, hW, hbdd, hdiv, hWr, hDVcont, hDWcont, hDVconv, hDWconv of CIV.false_of_finite_contradiction_data, in that order, with M = L, Vn n = V_{φ n}, DVn n = ∇V_{φ n} and DWn n = ∇W_{φ n}.

The endpoint vanishing on the axis segment

theorem CIV.step_finite_endpoint {A L : ℝ} (hA : 0 < A) (hL : 0 ≤ L) (Vseq Wseq : ℕ → ℝ × ℝ → ℝ) (hVsmooth : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (Vseq n)) (hWsmooth : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (Wseq n)) (hVbdd : ∀ (j : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ y ∈ halfPlaneRectangle j, |Vseq n y| ≤ L ∧ ‖fderiv ℝ (Vseq n) y‖ ≤ L ∧ ‖fderiv ℝ (fderiv ℝ (Vseq n)) y‖ ≤ L) (hWbdd : ∀ (j : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ y ∈ halfPlaneRectangle j, |Wseq n y| ≤ L ∧ ‖fderiv ℝ (Wseq n) y‖ ≤ L ∧ ‖fderiv ℝ (fderiv ℝ (Wseq n)) y‖ ≤ L) (haxis : ∀ (n : ℕ), Vseq n (0, 0) = 0) (hdivn : ∀ (p : ℝ × ℝ), 0 < p.1 → ∀ᶠ (n : ℕ) in Filter.atTop, (fderiv ℝ (Vseq n) p) (1, 0) + Vseq n p / p.1 + (fderiv ℝ (Wseq n) p) (0, 1) = 0) (hdWn : ∀ (p : ℝ × ℝ), 0 < p.1 → Filter.Tendsto (fun (n : ℕ) => (fderiv ℝ (Wseq n) p) (1, 0)) Filter.atTop (nhds 0)) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ TendstoUniformlyOn (fun (n : ℕ) (p : ℝ × ℝ) => (fderiv ℝ (Vseq (φ n)) p) (1, 0)) (fun (x : ℝ × ℝ) => 0) Filter.atTop (Set.Icc 0 A ×ˢ {0}) ∧ TendstoUniformlyOn (fun (n : ℕ) (p : ℝ × ℝ) => (fderiv ℝ (Wseq (φ n)) p) (0, 1)) (fun (x : ℝ × ℝ) => 0) Filter.atTop (Set.Icc 0 A ×ˢ {0}) ∧ TendstoUniformlyOn (fun (n : ℕ) (p : ℝ × ℝ) => Vseq (φ n) p / p.1) (fun (x : ℝ × ℝ) => 0) Filter.atTop (Set.Icc 0 A ×ˢ {0})

eq:aniso:zoom:finite:endpoint on the segment [0, A] × {0}: along the subsequence of CIV.exists_subseq_finite_endpoint_data, the radial derivative ∂_R V_n, the axial derivative ∂_Z W_n and the quotient V_n/R all tend to zero uniformly there, the axis included.

The contradiction

theorem CIV.step_finite_contradiction {A c₀ L : ℝ} (hA : 0 < A) (hc₀ : 0 < c₀) (hL : 0 ≤ L) (Vseq Wseq : ℕ → ℝ × ℝ → ℝ) (hVsmooth : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (Vseq n)) (hWsmooth : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (Wseq n)) (hVbdd : ∀ (j : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ y ∈ halfPlaneRectangle j, |Vseq n y| ≤ L ∧ ‖fderiv ℝ (Vseq n) y‖ ≤ L ∧ ‖fderiv ℝ (fderiv ℝ (Vseq n)) y‖ ≤ L) (hWbdd : ∀ (j : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ y ∈ halfPlaneRectangle j, |Wseq n y| ≤ L ∧ ‖fderiv ℝ (Wseq n) y‖ ≤ L ∧ ‖fderiv ℝ (fderiv ℝ (Wseq n)) y‖ ≤ L) (haxis : ∀ (n : ℕ), Vseq n (0, 0) = 0) (hdivn : ∀ (p : ℝ × ℝ), 0 < p.1 → ∀ᶠ (n : ℕ) in Filter.atTop, (fderiv ℝ (Vseq n) p) (1, 0) + Vseq n p / p.1 + (fderiv ℝ (Wseq n) p) (0, 1) = 0) (hdWn : ∀ (p : ℝ × ℝ), 0 < p.1 → Filter.Tendsto (fun (n : ℕ) => (fderiv ℝ (Wseq n) p) (1, 0)) Filter.atTop (nhds 0)) {Rsel : ℕ → ℝ} (hRmem : ∀ (n : ℕ), Rsel n ∈ Set.Icc 0 A) (hlower : ∀ᶠ (n : ℕ) in Filter.atTop, c₀ ≤ 2 * |(fderiv ℝ (Vseq n) (Rsel n, 0)) (1, 0)| + |Vseq n (Rsel n, 0) / Rsel n| + |(fderiv ℝ (Wseq n) (Rsel n, 0)) (0, 1)|) : False

Step 2 of prop:aniso:small closes: a sequence of meridional fields (V_n, W_n) with the endpoint data of CIV.exists_subseq_finite_endpoint_data cannot satisfy the selection bound eq:aniso:zoom:selected at radii R_n ∈ [0, A]. The extraction supplies exactly the nine convergence and limit hypotheses of CIV.false_of_finite_contradiction_data, which then produces the contradiction.

The form produced by the selection bound

theorem CIV.step_finite_contradiction_of_dr_dz {A c₀ L : ℝ} (hA : 0 < A) (hc₀ : 0 < c₀) (hL : 0 ≤ L) (Vseq Wseq : ℕ → ℝ × ℝ → ℝ) (Vfield Wfield : ℕ → (ℝ × ℝ) × ℝ → ℝ) (hVslice : ∀ (n : ℕ) (q : ℝ × ℝ), Vfield n (q, -1) = Vseq n q) (hWslice : ∀ (n : ℕ) (q : ℝ × ℝ), Wfield n (q, -1) = Wseq n q) (hVsmooth : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (Vseq n)) (hWsmooth : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (Wseq n)) (hVbdd : ∀ (j : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ y ∈ halfPlaneRectangle j, |Vseq n y| ≤ L ∧ ‖fderiv ℝ (Vseq n) y‖ ≤ L ∧ ‖fderiv ℝ (fderiv ℝ (Vseq n)) y‖ ≤ L) (hWbdd : ∀ (j : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ y ∈ halfPlaneRectangle j, |Wseq n y| ≤ L ∧ ‖fderiv ℝ (Wseq n) y‖ ≤ L ∧ ‖fderiv ℝ (fderiv ℝ (Wseq n)) y‖ ≤ L) (haxis : ∀ (n : ℕ), Vseq n (0, 0) = 0) (hdivn : ∀ (p : ℝ × ℝ), 0 < p.1 → ∀ᶠ (n : ℕ) in Filter.atTop, (fderiv ℝ (Vseq n) p) (1, 0) + Vseq n p / p.1 + (fderiv ℝ (Wseq n) p) (0, 1) = 0) (hdWn : ∀ (p : ℝ × ℝ), 0 < p.1 → Filter.Tendsto (fun (n : ℕ) => (fderiv ℝ (Wseq n) p) (1, 0)) Filter.atTop (nhds 0)) {Rsel : ℕ → ℝ} (hRmem : ∀ (n : ℕ), Rsel n ∈ Set.Icc 0 A) (hlower : ∀ (n : ℕ), c₀ ≤ 2 * |dr (Vfield n) ((Rsel n, 0), -1)| + |Vfield n ((Rsel n, 0), -1) / Rsel n| + |dz (Wfield n) ((Rsel n, 0), -1)|) : False

The same contradiction, with the selected quantity written through the repository's dr, dz of the space-time fields at the selected time τ = -1: this is the form in which CIV.lt_of_neg_t_mul_meridionalQuantity_selection_lt delivers the lower bound eq:aniso:zoom:selected, with Vfield n = zoomV λ_n h z_n u and Wfield n = zoomW λ_n h z_n u and their τ = -1 slices as Vseq, Wseq.