The mixed-term estimate eq:aniso:closure:mixed:bound of lem:aniso:closure

This assembles the mixed-term bound of lem:aniso:closure from its four already-proved pieces:

• the z integration by parts of eq:aniso:closure:mixed (integral_cutoff_sq_stretchMixedTerm_eq);
• the swirl bound |u_θ| ≤ W on tsupport χ (hW, carried the same way energy_inequality_of_mixed_term_bound_of_split carries it);
• the representative-to-Cartesian L² transfer of CIV.Closure.MixedTermTransferBounds, feeding the elliptic and div–curl bounds of CIV.Closure.EllipticBoundsAnnulusBound;
• the elliptic Cauchy–Schwarz step (abs_integral_mul_le_sqrt_mul_sqrt) and the final Young's-inequality absorption (mixed_term_bound_of_cauchy_schwarz).

The ∂_zχ-carrying error term of the integration by parts is bounded separately, by a constant that does not depend on t (CIV.Closure.MixedTermErrorBound), from the same order-≤ 2 annulus data that supplies the elliptic bounds.

theorem CIV.step_closure_mixed_term {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) (haxi : IsAxisymmetricOn u 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) (hρpos : 0 < ρ) {t₀ : ℝ} (ht₀ : t₀ ∈ Set.Ioo (-1) 0) {A : Set CKN.Foundation.Parabolic.Vec3} (hAcl : IsClosed A) (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) {W : ℝ → ℝ} (hW : ∀ t ∈ Set.Ioo t₀ 0, ∀ (x₁ x₃ : ℝ), meridional x₁ x₃ ∈ CKN.Foundation.Parabolic.vec3Ball 0 ρ → |u (meridional x₁ x₃, t) 1| ≤ W t) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ t ∈ Set.Ioo t₀ 0, |∫ (x : CKN.Foundation.Parabolic.Vec3), χ x ^ 2 * stretchMixedTerm u x t| ≤ 1 / 4 * cutoffEnstrophyDissipation χ u t + C * (W t ^ 2 + 1) * (cutoffEnstrophy χ u t + 1)

eq:aniso:closure:mixed:bound. For a classical solution with a cutoff χ supported in B(ρ), 0 < ρ, order-≤ 2 derivative bounds for u on the closed annulus A carrying ∇χ, and a swirl bound |u_θ| ≤ W on B(ρ), the mixed summand I(t) = ∫ χ² (∂_r u_z) ω_r ω_z of the tested vortex-stretching term satisfies I(t) ≤ (1/4) M(t) + C (W(t)² + 1) (Y(t) + 1) on (t₀, 0), for some C ≥ 0.