Receding Transport Pairing Bound

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

theorem CIV.transport_term_pairing_bound_fixed {C h lam rc zc : ℝ} (hC : 0 ≤ C) (hh0 : 0 ≤ h) (hh1 : h ≤ 1 / 2) (hlam : 0 < lam) (hdelta : lam ^ (2 * h) ≤ 1) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {K : Set (ℝ × ℝ)} (hK : IsCompact K) {τ : ℝ} (htau : τ ≤ -1) (hmem : ∀ y ∈ K, zoomPointRec lam h rc zc (y, τ) ∈ unitCylinder) (ψ : ℝ × ℝ → ℝ) (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 : ℝ × ℝ), -(dr (fun (q : (ℝ × ℝ) × ℝ) => zoomVRec lam h rc zc u q * zoomTheta lam h rc zc u q) (y, τ) + dz (fun (q : (ℝ × ℝ) × ℝ) => zoomWRec lam h rc zc u q * zoomTheta lam h rc zc u q) (y, τ)) * ψ y| ≤ 4 * C ^ 2 * (MeasureTheory.volume K).toReal * B

The transport/divergence-term pairing bound at a fixed zoom scale: the integral of −(∂_R(V_nΘ_n) + ∂_Z(W_nΘ_n)), the perfect-divergence transport term of zoomTheta_pde_divergenceForm, against a test function supported in the interior of a compact set K is bounded by 4C² times the bound B on ψ and its first two derivatives, times the volume of K.

theorem CIV.transport_term_pairing_bound {C h : ℝ} (hC : 0 ≤ C) (hh0 : 0 ≤ h) (hh1 : h ≤ 1 / 2) {rc zc : ℝ} (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} (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {K : Set (ℝ × ℝ)} (hK : IsCompact K) {τ : ℝ} (htau : τ ≤ -1) (hmem : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ y ∈ K, zoomPointRec (lam n) h rc zc (y, τ) ∈ unitCylinder) : ∃ (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 : ℝ × ℝ), -(dr (fun (q : (ℝ × ℝ) × ℝ) => zoomVRec (lam n) h rc zc u q * zoomTheta (lam n) h rc zc u q) (y, τ) + dz (fun (q : (ℝ × ℝ) × ℝ) => zoomWRec (lam n) h rc zc u q * zoomTheta (lam n) h rc zc u q) (y, τ)) * ψ y| ≤ C₀ * B

The eventual-in-n pairing bound for the transport/divergence term: C₀ := 4C² is chosen before n, matching the eventual form of the time-pairing estimate hpair.