The receding-axis contradiction

eq:aniso:zoom:receding:quotient: the final contradiction of the receding-axis case. In the recentred variables eq:aniso:zoom:receding:variables the selected point is the origin of ℝ × ℝ and the axis sits at R = -A_n, so the meridional fields live on the whole plane. The limiting divergence identity of eq:aniso:zoom:receding:div is ∂_R V + ∂_Z W = 0 with no radial quotient, the term V_n / (A_n + R) vanishing uniformly on compact sets because A_n → ∞ while V_n stays bounded. Endpoint vanishing is therefore CIV.endpoint_vanishing_rec, which holds at every point of the plane and needs no continuity statement at a boundary; and the radial quotient at the selected point is bounded by M / A_n. All three summands of eq:aniso:zoom:selected thus tend to 0.

theorem CIV.tendsto_at_of_tendstoUniformlyOn_const (S : Set (ℝ × ℝ)) (F : ℕ → ℝ × ℝ → ℝ) (c : ℝ) (hF : TendstoUniformlyOn F (fun (x : ℝ × ℝ) => c) Filter.atTop S) {x₀ : ℝ × ℝ} (hx₀ : x₀ ∈ S) : Filter.Tendsto (fun (n : ℕ) => F n x₀) Filter.atTop (nhds c)

Uniform convergence on a set to a constant implies pointwise convergence to that constant at every point of the set.

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

eq:aniso:zoom:receding:endpoint in pointwise form: a divergence-free meridional pair (V, W) on ℝ × ℝ with ∂_R W = 0 and V bounded has ∂_R V and ∂_Z W vanishing at every point, in particular at the origin, which is the selected point in the variables eq:aniso:zoom:receding:variables. The divergence hypothesis is the quotient-free identity of eq:aniso:zoom:receding:div.

theorem CIV.false_of_receding_contradiction_data {c₀ M : ℝ} (hc₀ : 0 < c₀) (V W : ℝ × ℝ → ℝ) (DV DW : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ) (hV : ∀ (p : ℝ × ℝ), HasFDerivAt V (DV p) p) (hW : ∀ (p : ℝ × ℝ), HasFDerivAt W (DW p) p) (hbdd : ∀ (p : ℝ × ℝ), |V p| ≤ M) (hdiv : ∀ (p : ℝ × ℝ), (DV p) (1, 0) + (DW p) (0, 1) = 0) (hWr : ∀ (p : ℝ × ℝ), (DW p) (1, 0) = 0) (DVn DWn : ℕ → ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ) (Vn : ℕ → ℝ × ℝ → ℝ) (S : Set (ℝ × ℝ)) (hS : (0, 0) ∈ S) (hDVconv : TendstoUniformlyOn DVn DV Filter.atTop S) (hDWconv : TendstoUniformlyOn DWn DW Filter.atTop S) {Anseq : ℕ → ℝ} (hAtop : Filter.Tendsto Anseq Filter.atTop Filter.atTop) (hApos : ∀ (n : ℕ), 0 < Anseq n) (hVnbdd : ∀ (n : ℕ), |Vn n (0, 0)| ≤ M) (hlower : ∀ (n : ℕ), c₀ ≤ |(DVn n (0, 0)) (1, 0)| + |Vn n (0, 0)| / Anseq n + |(DWn n (0, 0)) (0, 1)|) : False

The final contradiction of the receding-axis zoom. On a set S containing the selected point — the origin of the variables eq:aniso:zoom:receding:variables — the recentred derivatives converge uniformly to the endpoint derivatives, which vanish identically by eq:aniso:zoom:receding:endpoint; the radial quotient at the selected point is at most M / A_n with A_n → ∞, which is eq:aniso:zoom:receding:quotient. The three summands of eq:aniso:zoom:selected therefore tend to 0, and ge_of_tendsto' forces c₀ ≤ 0, contradicting hc₀.