Receding Swirl Pairing Bound

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

theorem CIV.swirl_term_pairing_bound_fixed {h lam rc zc CΓ : ℝ} (hCΓ : 0 ≤ CΓ) (hlam : 0 < lam) (hdelta : lam ^ (2 * h) ≤ 1) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {K : Set (ℝ × ℝ)} (hK : IsCompact K) {τ : ℝ} (hmem : ∀ y ∈ K, zoomPointRec lam h rc zc (y, τ) ∈ unitCylinder) (hΓ : ∀ y ∈ K, |circulation u (zoomPointRec lam h rc zc (y, τ))| ≤ CΓ) (hApos : ∀ y ∈ K, 1 ≤ rc / lam + y.1) (ψ : ℝ × ℝ → ℝ) (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hψU : tsupport ψ ⊆ interior K) (B : ℝ) : 0 ≤ B → ∀ (hψB : ∀ (y : ℝ × ℝ), |ψ y| ≤ B ∧ ‖fderiv ℝ ψ y‖ ≤ B ∧ ‖fderiv ℝ (fderiv ℝ ψ) y‖ ≤ B), |∫ (y : ℝ × ℝ), 1 / (rc / lam + y.1) * dz (fun (q : (ℝ × ℝ) × ℝ) => zoomSRec lam h rc zc u q ^ 2) (y, τ) * ψ y| ≤ CΓ ^ 2 * (MeasureTheory.volume K).toReal * B

The swirl-source pairing bound at a fixed zoom scale: the integral of the divergence-form swirl term (1/(A+R)) ∂_Z(S_n²) of zoomTheta_pde against a test function supported in the interior of a compact set K is bounded by CΓ² times the bound B on ψ and its first two derivatives, times the volume of K.

theorem CIV.swirl_term_pairing_bound {h rc zc CΓ : ℝ} (hCΓ : 0 ≤ CΓ) (lam : ℕ → ℝ) (hlam_pos : ∀ (n : ℕ), 0 < lam n) (hlam_le : ∀ᶠ (n : ℕ) in Filter.atTop, lam n ^ (2 * h) ≤ 1) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {K : Set (ℝ × ℝ)} (hK : IsCompact K) {τ : ℝ} (hmem : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ y ∈ K, zoomPointRec (lam n) h rc zc (y, τ) ∈ unitCylinder) (hΓ : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ y ∈ K, |circulation u (zoomPointRec (lam n) h rc zc (y, τ))| ≤ CΓ) (hApos : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ y ∈ K, 1 ≤ rc / lam n + y.1) : ∃ (C₀ : ℝ), 0 ≤ C₀ ∧ ∀ (ψ : ℝ × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ interior K → ∀ (B : ℝ), 0 ≤ B → (∀ (y : ℝ × ℝ), |ψ y| ≤ B ∧ ‖fderiv ℝ ψ y‖ ≤ B ∧ ‖fderiv ℝ (fderiv ℝ ψ) y‖ ≤ B) → ∀ᶠ (n : ℕ) in Filter.atTop, |∫ (y : ℝ × ℝ), 1 / (rc / lam n + y.1) * dz (fun (q : (ℝ × ℝ) × ℝ) => zoomSRec (lam n) h rc zc u q ^ 2) (y, τ) * ψ y| ≤ C₀ * B

The eventual-in-n pairing bound for the swirl term: C₀ := CΓ² is chosen before n, matching the eventual form of the time-pairing estimate hpair of the receding compactness.