Receding Dt Past Pairing Assembly

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

theorem CIV.dtPast_zoomTheta_pairing_bound_fixed {h lam rc zc : ℝ} (hlam : 0 < lam) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {pr : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hsol : IsClassicalSolutionOn u pr f unitCylinder) (haxi : IsAxisymmetricOn u unitCylinder) {K : Set (ℝ × ℝ)} {τ : ℝ} (hmem : ∀ y ∈ K, zoomPointRec lam h rc zc (y, τ) ∈ unitCylinder) (hApos : ∀ y ∈ K, 1 ≤ rc / lam + y.1) (ψ : ℝ × ℝ → ℝ) (hψU : tsupport ψ ⊆ interior K) (B C_transport C_diffusion C_curvature C_swirl C_force : ℝ) (T1 T2 T3 T4 T5 : ℝ × ℝ → ℝ) (hT1_def : T1 = fun (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, τ))) (hT2_def : T2 = fun (y : ℝ × ℝ) => dr (dr fun (q : (ℝ × ℝ) × ℝ) => zoomTheta lam h rc zc u q) (y, τ) + (lam ^ (2 * h)) ^ 2 * dz (dz fun (q : (ℝ × ℝ) × ℝ) => zoomTheta lam h rc zc u q) (y, τ)) (hT3_def : T3 = fun (y : ℝ × ℝ) => dr (fun (q : (ℝ × ℝ) × ℝ) => zoomTheta lam h rc zc u q) (y, τ) / (rc / lam + y.1) - zoomTheta lam h rc zc u (y, τ) / (rc / lam + y.1) ^ 2) (hT4_def : T4 = fun (y : ℝ × ℝ) => 1 / (rc / lam + y.1) * dz (fun (q : (ℝ × ℝ) × ℝ) => zoomSRec lam h rc zc u q ^ 2) (y, τ)) (hT5_def : T5 = fun (y : ℝ × ℝ) => lam ^ 4 * lam ^ (2 * h) * curlComp f 1 (zoomPointRec lam h rc zc (y, τ))) (hint1 : MeasureTheory.Integrable (fun (y : ℝ × ℝ) => T1 y * ψ y) MeasureTheory.volume) (hint2 : MeasureTheory.Integrable (fun (y : ℝ × ℝ) => T2 y * ψ y) MeasureTheory.volume) (hint3 : MeasureTheory.Integrable (fun (y : ℝ × ℝ) => T3 y * ψ y) MeasureTheory.volume) (hint4 : MeasureTheory.Integrable (fun (y : ℝ × ℝ) => T4 y * ψ y) MeasureTheory.volume) (hint5 : MeasureTheory.Integrable (fun (y : ℝ × ℝ) => T5 y * ψ y) MeasureTheory.volume) (hbound1 : |∫ (y : ℝ × ℝ), T1 y * ψ y| ≤ C_transport * B) (hbound2 : |∫ (y : ℝ × ℝ), T2 y * ψ y| ≤ C_diffusion * B) (hbound3 : |∫ (y : ℝ × ℝ), T3 y * ψ y| ≤ C_curvature * B) (hbound4 : |∫ (y : ℝ × ℝ), T4 y * ψ y| ≤ C_swirl * B) (hbound5 : |∫ (y : ℝ × ℝ), T5 y * ψ y| ≤ C_force * B) : |∫ (y : ℝ × ℝ), dtPast (fun (q : (ℝ × ℝ) × ℝ) => zoomTheta lam h rc zc u q) (y, τ) * ψ y| ≤ (C_transport + C_diffusion + C_curvature + C_swirl + C_force) * B

Assembling the five term-pairing bounds (transport/divergence, diffusion, curvature, swirl, force — each independently established) via zoomTheta_pde_divergenceForm into a single domination bound on ∫ (dtPast Θ_n)(·, τ) ψ, the time-pairing estimate hpair of the receding compactness. This is the pointwise derivative bound from the zoom PDE that CIV.hasDerivAt_integral_mul_testfunction_of_dominated differentiates under the integral sign, and that CIV.abs_sub_le_of_forall_hasDerivAt_le then turns into the literal hpair shape. Each of the five pieces is continuous with compact support (tsupport ψ), hence integrable; that fact is carried explicitly since the five term-pairing lemmas are proved separately.

theorem CIV.exists_dtPast_zoomTheta_pairing_bound_fixed {h lam rc zc : ℝ} (hlam : 0 < lam) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {pr : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hsol : IsClassicalSolutionOn u pr f unitCylinder) (haxi : IsAxisymmetricOn u unitCylinder) {K : Set (ℝ × ℝ)} {τ : ℝ} (hmem : ∀ y ∈ K, zoomPointRec lam h rc zc (y, τ) ∈ unitCylinder) (hApos : ∀ y ∈ K, 1 ≤ rc / lam + y.1) (ψ : ℝ × ℝ → ℝ) (hψU : tsupport ψ ⊆ interior K) (B C_transport C_diffusion C_curvature C_swirl C_force : ℝ) (hC_transport : 0 ≤ C_transport) (hC_diffusion : 0 ≤ C_diffusion) (hC_curvature : 0 ≤ C_curvature) (hC_swirl : 0 ≤ C_swirl) (hC_force : 0 ≤ C_force) (T1 T2 T3 T4 T5 : ℝ × ℝ → ℝ) (hT1_def : T1 = fun (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, τ))) (hT2_def : T2 = fun (y : ℝ × ℝ) => dr (dr fun (q : (ℝ × ℝ) × ℝ) => zoomTheta lam h rc zc u q) (y, τ) + (lam ^ (2 * h)) ^ 2 * dz (dz fun (q : (ℝ × ℝ) × ℝ) => zoomTheta lam h rc zc u q) (y, τ)) (hT3_def : T3 = fun (y : ℝ × ℝ) => dr (fun (q : (ℝ × ℝ) × ℝ) => zoomTheta lam h rc zc u q) (y, τ) / (rc / lam + y.1) - zoomTheta lam h rc zc u (y, τ) / (rc / lam + y.1) ^ 2) (hT4_def : T4 = fun (y : ℝ × ℝ) => 1 / (rc / lam + y.1) * dz (fun (q : (ℝ × ℝ) × ℝ) => zoomSRec lam h rc zc u q ^ 2) (y, τ)) (hT5_def : T5 = fun (y : ℝ × ℝ) => lam ^ 4 * lam ^ (2 * h) * curlComp f 1 (zoomPointRec lam h rc zc (y, τ))) (hint1 : MeasureTheory.Integrable (fun (y : ℝ × ℝ) => T1 y * ψ y) MeasureTheory.volume) (hint2 : MeasureTheory.Integrable (fun (y : ℝ × ℝ) => T2 y * ψ y) MeasureTheory.volume) (hint3 : MeasureTheory.Integrable (fun (y : ℝ × ℝ) => T3 y * ψ y) MeasureTheory.volume) (hint4 : MeasureTheory.Integrable (fun (y : ℝ × ℝ) => T4 y * ψ y) MeasureTheory.volume) (hint5 : MeasureTheory.Integrable (fun (y : ℝ × ℝ) => T5 y * ψ y) MeasureTheory.volume) (hbound1 : |∫ (y : ℝ × ℝ), T1 y * ψ y| ≤ C_transport * B) (hbound2 : |∫ (y : ℝ × ℝ), T2 y * ψ y| ≤ C_diffusion * B) (hbound3 : |∫ (y : ℝ × ℝ), T3 y * ψ y| ≤ C_curvature * B) (hbound4 : |∫ (y : ℝ × ℝ), T4 y * ψ y| ≤ C_swirl * B) (hbound5 : |∫ (y : ℝ × ℝ), T5 y * ψ y| ≤ C_force * B) : ∃ (C₀ : ℝ), 0 ≤ C₀ ∧ |∫ (y : ℝ × ℝ), dtPast (fun (q : (ℝ × ℝ) × ℝ) => zoomTheta lam h rc zc u q) (y, τ) * ψ y| ≤ C₀ * B

The existential form of dtPast_zoomTheta_pairing_bound_fixed, bundling its five explicit constants into the single ∃ C₀, 0 ≤ C₀ ∧ ... shape the domination hypothesis hdom of CIV.exists_time_pairing_bound_of_dtPast_bound_zoomTheta (CIV/Zoom/RecedingTimePairingWiring.lean) needs at a fixed τ.

theorem CIV.dtPast_zoomTheta_pairing_bound {h rc zc : ℝ} (lam : ℕ → ℝ) (hlam_pos : ∀ (n : ℕ), 0 < lam n) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {pr : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hsol : IsClassicalSolutionOn u pr f unitCylinder) (haxi : IsAxisymmetricOn u unitCylinder) {K : Set (ℝ × ℝ)} : IsCompact K → ∀ {τ : ℝ} (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) (ψ : ℝ × ℝ → ℝ), HasCompactSupport ψ → ∀ (hψU : tsupport ψ ⊆ interior K) (B C_transport C_diffusion C_curvature C_swirl C_force : ℝ) (T1 T2 T3 T4 T5 : ℕ → ℝ × ℝ → ℝ) (hT1_def : ∀ (n : ℕ), T1 n = fun (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, τ))) (hT2_def : ∀ (n : ℕ), T2 n = fun (y : ℝ × ℝ) => dr (dr fun (q : (ℝ × ℝ) × ℝ) => zoomTheta (lam n) h rc zc u q) (y, τ) + (lam n ^ (2 * h)) ^ 2 * dz (dz fun (q : (ℝ × ℝ) × ℝ) => zoomTheta (lam n) h rc zc u q) (y, τ)) (hT3_def : ∀ (n : ℕ), T3 n = fun (y : ℝ × ℝ) => dr (fun (q : (ℝ × ℝ) × ℝ) => zoomTheta (lam n) h rc zc u q) (y, τ) / (rc / lam n + y.1) - zoomTheta (lam n) h rc zc u (y, τ) / (rc / lam n + y.1) ^ 2) (hT4_def : ∀ (n : ℕ), T4 n = fun (y : ℝ × ℝ) => 1 / (rc / lam n + y.1) * dz (fun (q : (ℝ × ℝ) × ℝ) => zoomSRec (lam n) h rc zc u q ^ 2) (y, τ)) (hT5_def : ∀ (n : ℕ), T5 n = fun (y : ℝ × ℝ) => lam n ^ 4 * lam n ^ (2 * h) * curlComp f 1 (zoomPointRec (lam n) h rc zc (y, τ))) (hint : ∀ᶠ (n : ℕ) in Filter.atTop, MeasureTheory.Integrable (fun (y : ℝ × ℝ) => T1 n y * ψ y) MeasureTheory.volume ∧ MeasureTheory.Integrable (fun (y : ℝ × ℝ) => T2 n y * ψ y) MeasureTheory.volume ∧ MeasureTheory.Integrable (fun (y : ℝ × ℝ) => T3 n y * ψ y) MeasureTheory.volume ∧ MeasureTheory.Integrable (fun (y : ℝ × ℝ) => T4 n y * ψ y) MeasureTheory.volume ∧ MeasureTheory.Integrable (fun (y : ℝ × ℝ) => T5 n y * ψ y) MeasureTheory.volume) (hbound : ∀ᶠ (n : ℕ) in Filter.atTop, |∫ (y : ℝ × ℝ), T1 n y * ψ y| ≤ C_transport * B ∧ |∫ (y : ℝ × ℝ), T2 n y * ψ y| ≤ C_diffusion * B ∧ |∫ (y : ℝ × ℝ), T3 n y * ψ y| ≤ C_curvature * B ∧ |∫ (y : ℝ × ℝ), T4 n y * ψ y| ≤ C_swirl * B ∧ |∫ (y : ℝ × ℝ), T5 n y * ψ y| ≤ C_force * B), ∀ᶠ (n : ℕ) in Filter.atTop, |∫ (y : ℝ × ℝ), dtPast (fun (q : (ℝ × ℝ) × ℝ) => zoomTheta (lam n) h rc zc u q) (y, τ) * ψ y| ≤ (C_transport + C_diffusion + C_curvature + C_swirl + C_force) * B

The eventual-in-n domination bound: for a sequence of zoom scales, once the pointwise divergence-form identity, the membership/offset side conditions and the five term-pairing bounds all hold eventually, the same domination bound on ∫ (dtPast Θ_n)(·, τ) ψ holds eventually, with C₀ chosen before n, matching the eventual form of hpair's underlying derivative bound.