Receding Time Pairing Wiring

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

theorem CIV.exists_time_pairing_bound_of_dtPast_bound_zoomTheta {h lam rc zc : ℝ} {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) {a b : ℝ} (hab : a ≤ b) : b ≤ -1 → ∀ (hmem : ∀ y ∈ K, ∀ τ ∈ Set.Icc (a - 1 / 2) (b + 1 / 2), zoomPointRec lam h rc zc (y, τ) ∈ unitCylinder) {C₀ B : ℝ} (hC₀ : 0 ≤ C₀) (hB : 0 ≤ B) (ψ : ℝ × ℝ → ℝ) (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hψU : tsupport ψ ⊆ interior K) (hdom : ∀ τ ∈ Set.Icc a b, |∫ (y : ℝ × ℝ), dtPast (fun (q : (ℝ × ℝ) × ℝ) => zoomTheta lam h rc zc u q) (y, τ) * ψ y| ≤ C₀ * B), ∀ τ ∈ Set.Icc a b, ∀ τ' ∈ Set.Icc a b, |∫ (y : ℝ × ℝ), (zoomTheta lam h rc zc u (y, τ) - zoomTheta lam h rc zc u (y, τ')) * ψ y| ≤ C₀ * B * |τ - τ'|

The time-pairing bound for zoomTheta at a fixed zoom scale, on a compact time interval Icc a b ⊆ (-∞,-1]: a domination bound on ∫ (dtPast Θ)(·, τ) ψ for τ ∈ Icc a b gives, via differentiation under the integral sign and the mean value theorem, the literal two-point pairing bound hpair needs.