Documentation

LeanPool.CIVAxisymmetric.Closure.StretchingSplitIntegrated

The tested vortex-stretching term of eq:aniso:closure:tested, split #

The pointwise splitting stretching_eq_stretchGTerm of the vortex-stretching scalar (ω·∇u)·ω of eq:aniso:closure:stretch holds off the vertical axis. The axis is Lebesgue-null (ae_polarR_ne_zero), and each of the three summands is integrable against χ² because it is continuous on the unit ball and vanishes off the support of the cutoff. Integrating therefore turns the pointwise splitting into the identity

cutoffStretching χ u t = ∫ χ² G-term + I(t) - ∫ χ² 2 (u_θ ω_r/r) ω_θ,

with I(t) = ∫ χ² (∂_r u_z) ω_r ω_z the mixed term of eq:aniso:closure:mixed.

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

The mixed summand (∂_r u_z) ω_r ω_z of eq:aniso:closure:stretch, read at the meridional representative of x. Weighted by χ² and integrated it is the term I of eq:aniso:closure:mixed.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem CIV.continuousOn_stretchMixedTerm {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {t : ℝ} (ht : t ∈ Set.Ioo (-1) 0) :
    ContinuousOn (fun (x : CKN.Foundation.Parabolic.Vec3) => stretchMixedTerm u x t) (CKN.Foundation.Parabolic.vec3Ball 0 1)

    The mixed summand is continuous on the unit ball: it is built from continuous slices of ∇u and of the curl composed with the continuous representative map.

    source
    theorem CIV.integrable_cutoff_sq_stretchMixedTerm {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χs : HasCompactSupport χ) (hχU : tsupport χ ⊆ CKN.Foundation.Parabolic.vec3Ball 0 1) {t : ℝ} (ht : t ∈ Set.Ioo (-1) 0) :
    MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => χ x ^ 2 * stretchMixedTerm u x t) MeasureTheory.volume

    The χ²-weighted mixed summand is integrable.

    source
    theorem CIV.integrable_cutoff_sq_stretchGTerm {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) :
    MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => χ x ^ 2 * stretchGTerm u x t) MeasureTheory.volume

    The χ²-weighted four-term part is integrable.

    source
    theorem CIV.integrable_cutoff_sq_stretchAngular {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) :
    MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => χ x ^ 2 * (2 * stretchAngularSwirl u x t * curlComp u 1 (meridional (polarR x) (x 2), t))) MeasureTheory.volume

    The χ²-weighted angular summand is integrable.

    source
    theorem CIV.integrable_cutoff_sq_stretching {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χs : HasCompactSupport χ) (hχU : tsupport χ ⊆ CKN.Foundation.Parabolic.vec3Ball 0 1) {t : ℝ} (ht : t ∈ Set.Ioo (-1) 0) :
    MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => χ x ^ 2 * ∑ i : Fin 3, ∑ j : Fin 3, vorticityField u (x, t) j * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) j (x, t) * vorticityField u (x, t) i) MeasureTheory.volume

    The χ²-weighted vortex-stretching integrand is integrable.

    source
    theorem CIV.cutoffStretching_eq_stretchGTerm_add_mixed_sub_angular {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) :
    cutoffStretching χ u t = ((∫ (x : CKN.Foundation.Parabolic.Vec3), χ x ^ 2 * stretchGTerm u x t) + ∫ (x : CKN.Foundation.Parabolic.Vec3), χ x ^ 2 * stretchMixedTerm u x t) - ∫ (x : CKN.Foundation.Parabolic.Vec3), χ x ^ 2 * (2 * stretchAngularSwirl u x t * curlComp u 1 (meridional (polarR x) (x 2), t))

    eq:aniso:closure:stretch, integrated against χ². The tested vortex-stretching term of eq:aniso:closure:tested is the four-term part, plus the mixed term I of eq:aniso:closure:mixed, minus the angular term of eq:aniso:closure:angular:bound.