The curvature-term pairing bound with a general lower bound on the radius

The fixed-scale curvature-term pairing bound of CIV.Zoom.RecedingCurvaturePairingBound, with the offset A + R of eq:aniso:zoom:receding:equation bounded below by an arbitrary ε > 0 rather than by 1. With A = 0 this is the bound used on compact subsets of the open half-plane in the finite-axis compactness argument eq:aniso:zoom:finite:compactness.

theorem CIV.curvature_term_pairing_bound_fixed_of_le {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ε : 0 < ε) (hApos : ∀ y ∈ K, ε ≤ 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.