Locally uniform extraction on the half-plane from eventual bounds

The compactness step eq:aniso:zoom:finite:compactness of Step 2 of the proof of prop:aniso:small, in the form in which the zoom data supply it: the uniform bound, the uniform spatial Lipschitz bound and the time-pairing bound on a compact subset of the open half-plane hold only for all large n (the zoom preimage of the unit cylinder exhausts the half-plane only as n → ∞). This is the half-plane counterpart of CIV.exists_subseq_tendstoUniformlyOn_of_lipschitz_of_pairings_plane_eventually, and the eventual counterpart of CIV.exists_subseq_tendstoUniformlyOn_of_lipschitz_of_pairings.

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

The closed rectangles [1/(j+1), j+1] × [-(j+1), j+1] exhausting the open half-plane.

Equations

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

theorem CIV.isCompact_halfBox (j : ℕ) : IsCompact (halfBox j)

theorem CIV.pos_of_mem_halfBox {j : ℕ} {y : ℝ × ℝ} (hy : y ∈ halfBox j) : 0 < y.1

theorem CIV.one_zero_mem_halfBox (j : ℕ) : (1, 0) ∈ halfBox j

theorem CIV.halfBox_subset_interior_succ (j : ℕ) : halfBox j ⊆ interior (halfBox (j + 1))

theorem CIV.left_mem_planeTimeInterval' (j : ℕ) : -(↑j + 1) ∈ planeTimeInterval j

theorem CIV.le_of_mem_planeTimeInterval' {j : ℕ} {τ : ℝ} (hτ : τ ∈ planeTimeInterval j) : τ ≤ -1

theorem CIV.exists_nat_halfBox_bounds {a b c : ℝ} (ha : 0 < a) : ∃ (j : ℕ), 1 / (↑j + 1) < a ∧ a < ↑j + 1 ∧ b < ↑j + 1 ∧ c < ↑j + 1

A point of {R > 0} with bounded coordinates lies strictly inside some halfBox j.

theorem CIV.exists_subset_halfBox_prod {C : Set ((ℝ × ℝ) × ℝ)} (hC : IsCompact C) (hCsub : C ⊆ {q : (ℝ × ℝ) × ℝ | 0 < q.1.1 ∧ q.2 ≤ -1}) : ∃ (j : ℕ), C ⊆ halfBox j ×ˢ planeTimeInterval j

A compact subset of {R > 0, τ ≤ -1} lies in some halfBox j ×ˢ planeTimeInterval j.

theorem CIV.exists_subseq_tendstoUniformlyOn_of_lipschitz_of_pairings_eventually (Θ : ℕ → (ℝ × ℝ) × ℝ → ℝ) (hbdd : ∀ (K : Set (ℝ × ℝ)), IsCompact K → (∀ y ∈ K, 0 < y.1) → ∀ (J : Set ℝ), IsCompact J → (∀ τ ∈ J, τ ≤ -1) → ∃ (M : ℝ), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ y ∈ K, ∀ τ ∈ J, |Θ n (y, τ)| ≤ M) (hlip : ∀ (K : Set (ℝ × ℝ)), IsCompact K → (∀ y ∈ K, 0 < y.1) → ∀ (J : Set ℝ), IsCompact J → (∀ τ ∈ J, τ ≤ -1) → ∃ (L : ℝ), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ τ ∈ J, LipschitzOnWith L.toNNReal (fun (y : ℝ × ℝ) => Θ n (y, τ)) K) (hpair : ∀ (K : Set (ℝ × ℝ)), IsCompact K → (∀ y ∈ K, 0 < y.1) → ∀ (J : Set ℝ), IsCompact J → (∀ τ ∈ J, τ ≤ -1) → ∃ (Cₒ : ℝ), 0 ≤ Cₒ ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (ψ : ℝ × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ interior K → ∀ (B : ℝ), 0 ≤ B → (∀ (y : ℝ × ℝ), |ψ y| ≤ B ∧ ‖fderiv ℝ ψ y‖ ≤ B ∧ ‖fderiv ℝ (fderiv ℝ ψ) y‖ ≤ B) → ∀ τ ∈ J, ∀ τ' ∈ J, |∫ (y : ℝ × ℝ), (Θ n (y, τ) - Θ n (y, τ')) * ψ y| ≤ Cₒ * B * |τ - τ'|) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∃ (Ω : (ℝ × ℝ) × ℝ → ℝ), ContinuousOn Ω {q : (ℝ × ℝ) × ℝ | 0 < q.1.1 ∧ q.2 ≤ -1} ∧ ∀ (C : Set ((ℝ × ℝ) × ℝ)), IsCompact C → C ⊆ {q : (ℝ × ℝ) × ℝ | 0 < q.1.1 ∧ q.2 ≤ -1} → TendstoUniformlyOn (fun (n : ℕ) => Θ (φ n)) Ω Filter.atTop C

eq:aniso:zoom:finite:compactness from eventual bounds: a sequence which on every compact subset of the open half-plane and every compact time set in (-∞, -1] is eventually uniformly bounded, eventually uniformly Lipschitz in space and eventually obeys the pairing bound in time, has a subsequence converging uniformly on every compact subset of {R > 0} × ℝ × (-∞, -1], to a limit continuous there.