C¹ extraction on the closed half-plane

A sequence of smooth functions on ℝ × ℝ whose values, gradients and second derivatives are bounded by one constant L on each of the squares [0, j+1] × [-(j+1), j+1] — 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 the closed half-plane {R ≥ 0} and is differentiable at every point of the open half-plane {R > 0}, with derivative the limit of the gradients.

This is C¹ compactness on compact subsets of the closed half-plane, so the limit and the convergence reach the axis {R = 0}; only the identification of the limit of the gradients with a derivative is restricted to the open half-plane, where the squares have interior points.

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.

Uniform convergence into a product

theorem CIV.tendstoUniformlyOn_prod_mk {ι : Type u_1} {X : Type u_2} {α : Type u_3} {β : Type u_4} [PseudoMetricSpace α] [PseudoMetricSpace β] {F : ι → X → α} {G : ι → X → β} {f : X → α} {g : X → β} {p : Filter ι} {s : Set X} (hF : TendstoUniformlyOn F f p s) (hG : TendstoUniformlyOn G g p s) : TendstoUniformlyOn (fun (n : ι) (x : X) => (F n x, G n x)) (fun (x : X) => (f x, g x)) p s

Uniform convergence of two families into pseudometric spaces gives uniform convergence of the pair, along the same filter.

The exhausting squares of the closed half-plane

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

The closed squares [0, j+1] × [-(j+1), j+1], which exhaust the closed half-plane {p : ℝ × ℝ | 0 ≤ p.1} and whose interiors exhaust the open half-plane {0 < p.1}.

Equations

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

theorem CIV.isCompact_halfPlaneRectangle (j : ℕ) : IsCompact (halfPlaneRectangle j)

theorem CIV.convex_halfPlaneRectangle (j : ℕ) : Convex ℝ (halfPlaneRectangle j)

theorem CIV.nonneg_of_mem_halfPlaneRectangle {j : ℕ} {p : ℝ × ℝ} (hp : p ∈ halfPlaneRectangle j) : 0 ≤ p.1

theorem CIV.exists_mem_halfPlaneRectangle {p : ℝ × ℝ} (hp : 0 ≤ p.1) : ∃ (j : ℕ), p ∈ halfPlaneRectangle j

Every point of the closed half-plane lies in one of the squares.

theorem CIV.exists_mem_interior_halfPlaneRectangle {p : ℝ × ℝ} (hp : 0 < p.1) : ∃ (j : ℕ), p ∈ interior (halfPlaneRectangle j)

Every point of the open half-plane lies in the interior of one of the squares.

theorem CIV.segment_subset_halfPlaneRectangle {A : ℝ} {j : ℕ} (hA : A ≤ ↑j + 1) : Set.Icc 0 A ×ˢ {0} ⊆ halfPlaneRectangle j

The segment [0, A] × {0} of the axis line sits inside every square of index at least A.

The extraction

theorem CIV.exists_subseq_tendstoUniformlyOn_c1_halfPlane (Vseq : ℕ → ℝ × ℝ → ℝ) (L : ℝ) (hL : 0 ≤ L) (hsmooth : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (Vseq n)) (hbdd : ∀ (j : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ y ∈ halfPlaneRectangle 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 (halfPlaneRectangle j)) ∧ (∀ (j : ℕ), TendstoUniformlyOn (fun (n : ℕ) => fderiv ℝ (Vseq (φ n))) DV Filter.atTop (halfPlaneRectangle j)) ∧ (∀ (j : ℕ), ContinuousOn DV (halfPlaneRectangle j)) ∧ (∀ (p : ℝ × ℝ), 0 ≤ p.1 → |V p| ≤ L) ∧ ∀ (p : ℝ × ℝ), 0 < p.1 → HasFDerivAt V (DV p) p

C¹ compactness on the closed half-plane: from a sequence of smooth functions whose value, gradient and second derivative are bounded by L on each square [0, j+1] × [-(j+1), j+1] for all large n, one subsequence converges together with its gradient, uniformly on every square. The limit obeys the same bound on the closed half-plane, its gradient limit is continuous on each square, and at every point of the open half-plane the limit is differentiable with derivative the limit of the gradients.

theorem CIV.tendstoUniformlyOn_comp_strictMono {X : Type u_1} {α : Type u_2} [UniformSpace α] {F : ℕ → X → α} {f : X → α} {s : Set X} (hF : TendstoUniformlyOn F f Filter.atTop s) {ψ : ℕ → ℕ} (hψ : StrictMono ψ) : TendstoUniformlyOn (fun (n : ℕ) => F (ψ n)) f Filter.atTop s

A subsequence of a uniformly convergent sequence converges uniformly to the same limit.