Receding Curvature Pairing Bound

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

theorem CIV.curvature_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) (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 : ℝ × ℝ), (dr (zoomTheta lam h rc zc u) (y, τ) / (rc / lam + y.1) - zoomTheta lam h rc zc u (y, τ) / (rc / lam + y.1) ^ 2) * ψ y| ≤ 2 * C * (MeasureTheory.volume K).toReal * B

The curvature-term pairing bound at a fixed zoom scale: the integral of the curvature term ∂_R Θ_n / (A + R) − Θ_n / (A + R)² of zoomTheta_pde against a test function supported in the interior of a compact set K is bounded by 2C times the bound B on ψ and its first two derivatives, times the volume of K.

theorem CIV.curvature_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) (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 : ℝ × ℝ), (dr (zoomTheta (lam n) h rc zc u) (y, τ) / (rc / lam n + y.1) - zoomTheta (lam n) h rc zc u (y, τ) / (rc / lam n + y.1) ^ 2) * ψ y| ≤ C₀ * B

The eventual-in-n pairing bound for the curvature term: C₀ := 2C is chosen before n, matching the eventual restatement hpair needs on an exhausting family.