Uniform convergence along a varying point

theorem CIV.tendsto_of_tendstoUniformlyOn_of_mem_forall (S : Set (ℝ × ℝ)) (F : ℕ → ℝ × ℝ → ℝ) (f : ℝ × ℝ → ℝ) (hF : TendstoUniformlyOn F f Filter.atTop S) {x : ℕ → ℝ × ℝ} (hx : ∀ (n : ℕ), x n ∈ S) : Filter.Tendsto (fun (n : ℕ) => F n (x n) - f (x n)) Filter.atTop (nhds 0)

If F n converges uniformly to f on a set S and x n ∈ S for all n, then F n (x n) - f (x n) → 0. This is the elementary fact that pointwise convergence along a sequence of points in the domain follows from uniform convergence on that domain.

Vanishing of the absolute value along a varying point

theorem CIV.abs_tendsto_zero_of_tendstoUniformlyOn_zero (S : Set (ℝ × ℝ)) (F : ℕ → ℝ × ℝ → ℝ) (hF : TendstoUniformlyOn F (fun (x : ℝ × ℝ) => 0) Filter.atTop S) {x : ℕ → ℝ × ℝ} (hx : ∀ (n : ℕ), x n ∈ S) : Filter.Tendsto (fun (n : ℕ) => |F n (x n)|) Filter.atTop (nhds 0)

If F n converges uniformly to 0 on a set S and x n ∈ S for all n, then |F n (x n)| → 0. Follows directly from the previous lemma.

Final contradiction of Step 2

theorem CIV.false_of_finite_contradiction_data {A c₀ : ℝ} (hA : 0 < A) (hc₀ : 0 < c₀) (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) (hDVcont : ContinuousOn (fun (r : ℝ) => (DV (r, 0)) (1, 0)) (Set.Icc 0 A)) (hDWcont : ContinuousOn (fun (r : ℝ) => (DW (r, 0)) (0, 1)) (Set.Icc 0 A)) (Vn : ℕ → ℝ × ℝ → ℝ) (DVn DWn : ℕ → ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ) (hDVconv : TendstoUniformlyOn DVn DV Filter.atTop (Set.Icc 0 A ×ˢ {0})) (hDWconv : TendstoUniformlyOn DWn DW Filter.atTop (Set.Icc 0 A ×ˢ {0})) (haxis : ∀ (n : ℕ), Vn n (0, 0) = 0) (hVncont : ∀ (n : ℕ), ContinuousOn (fun (r : ℝ) => Vn n (r, 0)) (Set.Icc 0 A)) (hVnderiv : ∀ (n : ℕ) (p : ℝ × ℝ), 0 < p.1 → HasFDerivAt (Vn n) (DVn n p) p) {R : ℕ → ℝ} (hRmem : ∀ (n : ℕ), R n ∈ Set.Icc 0 A) (hlower : ∀ᶠ (n : ℕ) in Filter.atTop, c₀ ≤ 2 * |(DVn n (R n, 0)) (1, 0)| + |Vn n (R n, 0) / R n| + |(DWn n (R n, 0)) (0, 1)|) : False

The final contradiction of the finite-axis zoom. The endpoint theorem CIV.endpoint_tendstoUniformlyOn_triple makes the radial derivative, the radial quotient and the axial derivative converge uniformly to 0 on [0, A] × {0}, hence along the selected sequence (R n, 0), while hlower keeps their combination at least c₀ > 0.

hlower carries the factor 2 on the radial derivative, which is the form in which CIV.neg_t_mul_meridionalQuantity_selection_le bounds the selected quantity of eq:aniso:zoom:selected. On the axis the manuscript's u_r / r is ∂_r u_r (CIV.radialQuotient_on_axis), whereas the quotient Vn n (R n, 0) / R n written here is 0 at R n = 0; the doubled radial derivative is what carries that summand across the axis. All three terms tend to 0, so the factor costs nothing here.