The z integration by parts of eq:aniso:closure:mixed

The mixed summand of the tested vortex-stretching term is

I = ∫ χ² (∂_r u_z) ω_r ω_z dx.

Off the axis ω_r = -∂_z u_θ (eq:aniso:vorticity, curlComp_zero_meridional), and the axis is Lebesgue-null, so I = -∫ χ² (∂_r u_z) (∂_z u_θ) ω_z dx. Integrating by parts in the vertical direction moves ∂_z off the swirl:

I = ∫ u_θ ∂_z(χ² (∂_r u_z) ω_z) dx,

which is eq:aniso:closure:mixed. There is no boundary term because the factor carrying the cutoff is compactly supported.

Every quantity here is a cylindrical scalar, read at the meridional representative meridional (polarR x) (x 2) of x. The representative map does not move the vertical coordinate, so such a composite has a vertical line derivative at every point — including on the axis, where the representative map is not differentiable — and that line derivative is the vertical derivative of the meridional quantity at the representative. Mathlib's integration by parts for line derivatives is exactly what this needs.

Vertical line derivatives of meridional quantities

theorem CIV.polarR_add_smul_basisVec_two (x : CKN.Foundation.Parabolic.Vec3) (s : ℝ) : polarR (x + s • CKN.basisVec 2) = polarR x

Shifting a point vertically does not change its polar radius.

theorem CIV.apply_two_add_smul_basisVec_two (x : CKN.Foundation.Parabolic.Vec3) (s : ℝ) : (x + s • CKN.basisVec 2) 2 = x 2 + s

Shifting a point vertically shifts its vertical coordinate.

theorem CIV.meridional_add_smul_basisVec_two (r z s : ℝ) : meridional r (z + s) = meridional r z + s • CKN.basisVec 2

A vertical shift of a meridional point is the meridional point of the shifted height.

theorem CIV.hasLineDerivAt_comp_polarRRep {F : CKN.Foundation.Parabolic.Vec3 → ℝ} {x : CKN.Foundation.Parabolic.Vec3} (hF : DifferentiableAt ℝ F (meridional (polarR x) (x 2))) : HasLineDerivAt ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => F (meridional (polarR y) (y 2))) ((fderiv ℝ F (meridional (polarR x) (x 2))) (CKN.basisVec 2)) x (CKN.basisVec 2)

A meridional quantity composed with the representative map has a vertical line derivative at every point, namely the vertical derivative of the quantity at the representative.

theorem CIV.hasLineDerivAt_mul {f g : CKN.Foundation.Parabolic.Vec3 → ℝ} {f' g' : ℝ} {x v : CKN.Foundation.Parabolic.Vec3} (hf : HasLineDerivAt ℝ f f' x v) (hg : HasLineDerivAt ℝ g g' x v) : HasLineDerivAt ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => f y * g y) (f' * g x + f x * g') x v

The Leibniz rule for line derivatives.

theorem CIV.hasLineDerivAt_const_zero (x v : CKN.Foundation.Parabolic.Vec3) : HasLineDerivAt ℝ (fun (x : CKN.Foundation.Parabolic.Vec3) => 0) 0 x v

A constant has vanishing line derivative.

Smoothness of the derivative slices

theorem CIV.contDiffOn_slice_partial {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (i j : Fin 3) {t : ℝ} (ht : t ∈ Set.Ioo (-1) 0) : ContDiffOn ℝ (↑⊤) (fun (y : CKN.Foundation.Parabolic.Vec3) => CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) j (y, t)) (CKN.Foundation.Parabolic.vec3Ball 0 1)

A spatial derivative of the velocity slice is smooth on the unit ball.

theorem CIV.contDiffOn_slice_curl {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (i : Fin 3) {t : ℝ} (ht : t ∈ Set.Ioo (-1) 0) : ContDiffOn ℝ (↑⊤) (fun (y : CKN.Foundation.Parabolic.Vec3) => curlComp u i (y, t)) (CKN.Foundation.Parabolic.vec3Ball 0 1)

The vorticity slice is smooth on the unit ball.

theorem CIV.differentiableAt_slice_partial {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (i j : Fin 3) {t : ℝ} (ht : t ∈ Set.Ioo (-1) 0) {y : CKN.Foundation.Parabolic.Vec3} (hy : y ∈ CKN.Foundation.Parabolic.vec3Ball 0 1) : DifferentiableAt ℝ (fun (y' : CKN.Foundation.Parabolic.Vec3) => CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) j (y', t)) y

A spatial derivative of the velocity slice is differentiable inside the unit ball.

theorem CIV.differentiableAt_slice_component {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (i : Fin 3) {t : ℝ} (ht : t ∈ Set.Ioo (-1) 0) {y : CKN.Foundation.Parabolic.Vec3} (hy : y ∈ CKN.Foundation.Parabolic.vec3Ball 0 1) : DifferentiableAt ℝ (fun (y' : CKN.Foundation.Parabolic.Vec3) => u (y', t) i) y

The velocity slice is differentiable inside the unit ball.

theorem CIV.differentiableAt_slice_curl {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (i : Fin 3) {t : ℝ} (ht : t ∈ Set.Ioo (-1) 0) {y : CKN.Foundation.Parabolic.Vec3} (hy : y ∈ CKN.Foundation.Parabolic.vec3Ball 0 1) : DifferentiableAt ℝ (fun (y' : CKN.Foundation.Parabolic.Vec3) => curlComp u i (y', t)) y

The vorticity slice is differentiable inside the unit ball.

The factor carried by the cutoff, and its vertical derivative

noncomputable def CIV.mixedTermFactor (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (χ : CKN.Foundation.Parabolic.Vec3 → ℝ) (x : CKN.Foundation.Parabolic.Vec3) (t : ℝ) : ℝ

The factor χ² (∂_r u_z) ω_z of eq:aniso:closure:mixed, read at the meridional representative of x.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CIV.mixedTermFactorDz (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (χ : CKN.Foundation.Parabolic.Vec3 → ℝ) (x : CKN.Foundation.Parabolic.Vec3) (t : ℝ) : ℝ

The vertical derivative ∂_z (χ² (∂_r u_z) ω_z) of eq:aniso:closure:mixed: the cutoff error term carrying ∂_zχ, and the two terms carrying ∂_z∂_r u_z and ∂_z ω_z.

Equations

• One or more equations did not get rendered due to their size.

theorem CIV.mixedTermFactor_eq_zero_of_notMem_tsupport {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {χ : CKN.Foundation.Parabolic.Vec3 → ℝ} {x : CKN.Foundation.Parabolic.Vec3} (hx : x ∉ tsupport χ) (t : ℝ) : mixedTermFactor u χ x t = 0

The cutoff-carrying factor vanishes off the support of the cutoff.

theorem CIV.mixedTermFactorDz_eq_zero_of_notMem_tsupport {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {χ : CKN.Foundation.Parabolic.Vec3 → ℝ} {x : CKN.Foundation.Parabolic.Vec3} (hx : x ∉ tsupport χ) (t : ℝ) : mixedTermFactorDz u χ x t = 0

Its vertical derivative vanishes off the support of the cutoff.

theorem CIV.tsupport_mixedTermFactor_subset (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (χ : CKN.Foundation.Parabolic.Vec3 → ℝ) (t : ℝ) : (tsupport fun (x : CKN.Foundation.Parabolic.Vec3) => mixedTermFactor u χ x t) ⊆ tsupport χ

The cutoff-carrying factor is supported inside the support of the cutoff.

theorem CIV.hasLineDerivAt_mixedTermFactor {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {χ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hχU : tsupport χ ⊆ CKN.Foundation.Parabolic.vec3Ball 0 1) {t : ℝ} (ht : t ∈ Set.Ioo (-1) 0) (x : CKN.Foundation.Parabolic.Vec3) : HasLineDerivAt ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => mixedTermFactor u χ y t) (mixedTermFactorDz u χ x t) x (CKN.basisVec 2)

The vertical line derivative of χ² (∂_r u_z) ω_z. The cutoff is globally smooth and the two meridional factors are smooth at the representative of every point of the support of the cutoff; off that support the factor vanishes identically nearby.

Continuity and integrability of the three integrands

eq:aniso:closure:mixed

theorem CIV.integral_cutoff_sq_stretchMixedTerm_eq {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (haxi : IsAxisymmetricOn u unitCylinder) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {χ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hχs : HasCompactSupport χ) (hχU : tsupport χ ⊆ CKN.Foundation.Parabolic.vec3Ball 0 1) {t : ℝ} (ht : t ∈ Set.Ioo (-1) 0) : ∫ (x : CKN.Foundation.Parabolic.Vec3), χ x ^ 2 * stretchMixedTerm u x t = ∫ (x : CKN.Foundation.Parabolic.Vec3), u (meridional (polarR x) (x 2), t) 1 * mixedTermFactorDz u χ x t

eq:aniso:closure:mixed. The mixed summand I = ∫ χ² (∂_r u_z) ω_r ω_z of the tested vortex-stretching term equals ∫ u_θ ∂_z(χ² (∂_r u_z) ω_z): off the axis ω_r = -∂_z u_θ, the axis is Lebesgue-null, and the vertical integration by parts has no boundary term because the factor carrying the cutoff is compactly supported.