The ∂_zχ-carrying error term of eq:aniso:closure:mixed:bound is a plain constant

mixedTermFactorDz's first summand carries ∂_zχ, hence is supported in a closed set A on which the order-≤ 2 annulus data of lem:aniso:annulus bounds every factor: u_θ, ∂_r u_z and ω_z, all read at the meridional representative, together with χ and ∂_zχ themselves, which are globally bounded because χ is smooth with compact support. Multiplying these uniform bounds by the (finite, time-independent) L¹ norm ∫ |χ| |∂_zχ| — rather than by the measure of A, which need not be tracked — bounds the whole error integral by a constant that does not depend on t.

theorem CIV.exists_abs_integral_swirl_mul_dzChi_error_le {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hsol : IsClassicalSolutionOn u p f unitCylinder) {χ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hχs : HasCompactSupport χ) {ρ : ℝ} (hρU : tsupport χ ⊆ CKN.Foundation.Parabolic.vec3Ball 0 ρ) (hρ1 : CKN.Foundation.Parabolic.vec3Ball 0 ρ ⊆ CKN.Foundation.Parabolic.vec3Ball 0 1) {t₀ : ℝ} (ht₀ : t₀ ∈ Set.Ioo (-1) 0) {A : Set CKN.Foundation.Parabolic.Vec3} (hχA : ∀ x ∉ A, fderiv ℝ χ x = 0) {Rm Rp Mu : ℝ} (hMu : 0 ≤ Mu) (hAsub : A ⊆ {x : CKN.Foundation.Parabolic.Vec3 | Rm < CKN.Foundation.Parabolic.vec3EuclideanNorm x ∧ CKN.Foundation.Parabolic.vec3EuclideanNorm x < Rp}) (hbound : ∀ (x : CKN.Foundation.Parabolic.Vec3), Rm < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < Rp → ∀ t ∈ Set.Ioo t₀ 0, ∀ (i : Fin 3) (α : Fin 3 → ℕ), α 0 + α 1 + α 2 ≤ 2 → |multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) α (x, t)| ≤ Mu) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ t ∈ Set.Ioo t₀ 0, |∫ (x : CKN.Foundation.Parabolic.Vec3), u (meridional (polarR x) (x 2), t) 1 * (2 * χ x * (fderiv ℝ χ x) (CKN.basisVec 2) * (CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 2) 0 (meridional (polarR x) (x 2), t) * curlComp u 2 (meridional (polarR x) (x 2), t)))| ≤ C

The ∂_zχ-carrying error term of mixedTermFactorDz, weighted by u_θ at the representative, is bounded by a plain constant: it is supported in A, where the order-≤ 2 annulus data bounds u_θ, ∂_r u_z and ω_z uniformly, and χ, ∂_zχ are globally bounded.