Receding Force Pairing Bound

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

theorem CIV.force_term_pairing_bound {h rc zc : ℝ} (hh0 : 0 < h) (lam : ℕ → ℝ) (hlam_pos : ∀ (n : ℕ), 0 < lam n) (hlam_le : ∀ᶠ (n : ℕ) in Filter.atTop, lam n ≤ 1) {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hMf : ForceC2Bounded f) {K : Set (ℝ × ℝ)} (hK : IsCompact K) (τ : ℝ) (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 : ℝ × ℝ), lam n ^ 4 * lam n ^ (2 * h) * curlComp f 1 (zoomPointRec (lam n) h rc zc (y, τ)) * ψ y| ≤ C₀ * B