Receding Whole Plane Compactness

Supporting results for the Constantin–Ignatova–Vicol axisymmetric regularity theorem.

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

The closed square of half-width j + 1 used to exhaust the meridional plane.

Equations

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

def CIV.planeTimeInterval (j : ℕ) : Set ℝ

The compact interval from -(j + 1) to -1 used to exhaust ancient times.

Equations

• CIV.planeTimeInterval j = Set.Icc (-(↑j + 1)) (-1)

theorem CIV.isCompact_planeBox (j : ℕ) : IsCompact (planeBox j)

theorem CIV.isCompact_planeTimeInterval (j : ℕ) : IsCompact (planeTimeInterval j)

theorem CIV.exists_subset_planeBox_prod {C : Set ((ℝ × ℝ) × ℝ)} (hC : IsCompact C) (hCsub : ∀ q ∈ C, q.2 ≤ -1) : ∃ (j : ℕ), C ⊆ planeBox j ×ˢ planeTimeInterval j

theorem CIV.planeBox_subset_interior_biggerBox (j : ℕ) : planeBox j ⊆ interior (planeBox (j + 1))

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

theorem CIV.exists_subseq_tendstoUniformlyOn_of_lipschitz_of_pairings_plane_eventually (Θ : ℕ → (ℝ × ℝ) × ℝ → ℝ) (hbdd : ∀ (K : Set (ℝ × ℝ)), IsCompact K → ∀ (J : Set ℝ), IsCompact J → (∀ τ ∈ J, τ ≤ -1) → ∃ (M : ℝ), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ y ∈ K, ∀ τ ∈ J, |Θ n (y, τ)| ≤ M) (hlip : ∀ (K : Set (ℝ × ℝ)), IsCompact K → ∀ (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 → ∀ (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 : (ℝ × ℝ) × ℝ | q.2 ≤ -1} ∧ ∀ (C : Set ((ℝ × ℝ) × ℝ)), IsCompact C → C ⊆ {q : (ℝ × ℝ) × ℝ | q.2 ≤ -1} → TendstoUniformlyOn (fun (n : ℕ) => Θ (φ n)) Ω Filter.atTop C

A version of exists_subseq_tendstoUniformlyOn_of_lipschitz_of_pairings_plane where the three hypotheses hold only eventually (for large n), with the threshold chosen before the test function ψ and its bound B in hpair — matching the shape hbdd/hlip already use (the constant M/L/Cₒ and the eventual threshold are both chosen before the data they bound). For each box of the exhaustion the three eventual thresholds combine into one common threshold beyond which all three bounds hold with all-n shape; a modified sequence, zero before that threshold and equal to Θ after, then lets the original all-n theorem apply directly, and since uniform limits only depend on the tail, the extracted subsequence also converges for the original Θ.