C¹ extraction on the whole plane

The recentred variables eq:aniso:zoom:receding:variables put the selected point at the origin of ℝ × ℝ and send the axis to R = -A_n with A_n → ∞, so the meridional fields of the receding-axis case live on the whole plane and the compact sets that exhaust their domain are the centred squares [-(j+1), j+1]² rather than the half-plane squares of CIV.halfPlaneRectangle.

A sequence of smooth functions on ℝ × ℝ whose values, gradients and second derivatives are bounded by one constant L on each centred square — for all large n, the threshold being allowed to depend on the square — has a subsequence converging, together with its gradient, uniformly on every one of those squares. The limit is bounded by L on all of ℝ × ℝ and is differentiable at every point, since every point of the plane is interior to a centred square; this is the difference with the half-plane statement, where the axis is a boundary and the derivative is identified only off it.

The extraction on one square is CIV.exists_subseq_tendstoUniformlyOn_c1; the passage from one square to all of them at once is the diagonal extraction CIV.exists_subseq_tendstoUniformlyOn_forall_of_subseq, applied to the pair (V_n, ∇V_n) so that the function and its gradient are extracted along a single subsequence.

The whole statement is at a fixed value of any remaining parameter: no time variable occurs, and no equicontinuity in a parameter is claimed or used.

The centred squares

def CIV.planeRectangle (j : ℕ) : Set (ℝ × ℝ)

The closed squares [-(j+1), j+1] × [-(j+1), j+1], which exhaust ℝ × ℝ and whose interiors already do.

Equations

• CIV.planeRectangle j = Set.Icc (-(↑j + 1)) (↑j + 1) ×ˢ Set.Icc (-(↑j + 1)) (↑j + 1)

theorem CIV.isCompact_planeRectangle (j : ℕ) : IsCompact (planeRectangle j)

theorem CIV.convex_planeRectangle (j : ℕ) : Convex ℝ (planeRectangle j)

theorem CIV.zero_mem_planeRectangle (j : ℕ) : (0, 0) ∈ planeRectangle j

The selected point of the recentred variables is the origin, and it lies in every centred square.

theorem CIV.exists_mem_interior_planeRectangle (p : ℝ × ℝ) : ∃ (j : ℕ), p ∈ interior (planeRectangle j)

Every point of the plane is interior to one of the centred squares.

theorem CIV.exists_mem_planeRectangle (p : ℝ × ℝ) : ∃ (j : ℕ), p ∈ planeRectangle j

Every point of the plane lies in one of the centred squares.

theorem CIV.exists_planeRectangle_superset {K : Set (ℝ × ℝ)} (hK : IsCompact K) : ∃ (j : ℕ), K ⊆ planeRectangle j

A compact subset of the plane is contained in one of the centred squares.

The extraction

theorem CIV.exists_subseq_tendstoUniformlyOn_c1_plane (Vseq : ℕ → ℝ × ℝ → ℝ) (L : ℝ) (hL : 0 ≤ L) (hsmooth : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (Vseq n)) (hbdd : ∀ (j : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ y ∈ planeRectangle j, |Vseq n y| ≤ L ∧ ‖fderiv ℝ (Vseq n) y‖ ≤ L ∧ ‖fderiv ℝ (fderiv ℝ (Vseq n)) y‖ ≤ L) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∃ (V : ℝ × ℝ → ℝ) (DV : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ), (∀ (j : ℕ), TendstoUniformlyOn (fun (n : ℕ) => Vseq (φ n)) V Filter.atTop (planeRectangle j)) ∧ (∀ (j : ℕ), TendstoUniformlyOn (fun (n : ℕ) => fderiv ℝ (Vseq (φ n))) DV Filter.atTop (planeRectangle j)) ∧ (∀ (j : ℕ), ContinuousOn DV (planeRectangle j)) ∧ (∀ (p : ℝ × ℝ), |V p| ≤ L) ∧ ∀ (p : ℝ × ℝ), HasFDerivAt V (DV p) p

C¹ compactness on the plane: from a sequence of smooth functions whose value, gradient and second derivative are bounded by L on each centred square for all large n, one subsequence converges together with its gradient, uniformly on every centred square. The limit obeys the same bound everywhere, its gradient limit is continuous on each square, and the limit is differentiable at every point with derivative the limit of the gradients.