The local steps of the interior estimates

At a point (x, s) whose backward window B_bar(x, 2ρ) × [s - ρ², s] lies in the unit cylinder, where the velocity is bounded by Mu, the pointwise heat bound applied to the vorticity equation in divergence form (and to its first and second spatial derivatives) bounds the vorticity level at (x, s) by C ρ Λ + C / ρ, where Λ bounds the same level on the window. The factor ρ in front of Λ is what the weighted absorption consumes. These are the local steps of the interior estimates in the proof of lem:aniso:annulus.

theorem CIV.contDiffOn_serrinForceFlux {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hf : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => f z) unitCylinder) (i m : Fin 3) : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => serrinForceFlux f i m z) unitCylinder

The antisymmetric flux is smooth where its field is.

theorem CIV.abs_serrinForceFlux_le {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {z : CKN.Foundation.Parabolic.ParabolicPoint} {B : ℝ} (hB0 : 0 ≤ B) (hB : ∀ (k : Fin 3), |f z k| ≤ B) (i m : Fin 3) : |serrinForceFlux f i m z| ≤ B

The antisymmetric flux is bounded by any bound of the field components.

theorem CIV.abs_curlComp_le_vortSum0 (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) (i : Fin 3) : |curlComp u i z| ≤ vortSum0 u z

Each vorticity component is bounded by the level-zero sum.

theorem CIV.abs_serrinVortFlux_le {u f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {z : CKN.Foundation.Parabolic.ParabolicPoint} {Mu Λ B : ℝ} (hB0 : 0 ≤ B) (hu : ∀ (k : Fin 3), |u z k| ≤ Mu) (hω : vortSum0 u z ≤ Λ) (hf : ∀ (k : Fin 3), |f z k| ≤ B) (i m : Fin 3) : |serrinVortFlux u f i m z| ≤ 2 * Mu * Λ + B

The divergence-form flux of the vorticity equation is bounded by 2 Mu Λ + B.

theorem CIV.LS0_local_level0 : ∃ (C : ℝ), 0 < C ∧ ∀ (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3), IsClassicalSolutionOn u p f unitCylinder → ∀ (Mf Mu : ℝ), (∀ z ∈ unitCylinder, ∀ (i : Fin 3) (α : Fin 3 → ℕ), α 0 + α 1 + α 2 ≤ 2 → |multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => f w i) α z| ≤ Mf) → ∀ (x : CKN.Foundation.Parabolic.Vec3) (s ρ Λ : ℝ), 0 < ρ → ρ ≤ 1 → (∀ (y : CKN.Foundation.Parabolic.Vec3) (s' : ℝ), CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ 2 * ρ → s - ρ ^ 2 ≤ s' → s' ≤ s → (y, s') ∈ unitCylinder ∧ (∀ (i : Fin 3), |u (y, s') i| ≤ Mu) ∧ vortSum0 u (y, s') ≤ Λ) → vortSum0 u (x, s) ≤ C * (1 + Mu) * ρ * Λ + C * (1 + Mu + Mf) / ρ

The local step at level zero.

theorem CIV.abs_spatialPartial_curlComp_le_vortSum1 (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) : |CKN.spatialPartial (curlComp u i) j z| ≤ vortSum1 u z

Each first derivative of the vorticity is bounded by the level-one sum.

theorem CIV.abs_spatialPartial_le_velSum1 (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) : |CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) j z| ≤ velSum1 u z

Each first derivative of the velocity is bounded by the level-one velocity sum.

theorem CIV.abs_spatialPartial_serrinForceFlux_le {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {z : CKN.Foundation.Parabolic.ParabolicPoint} {B : ℝ} (hB0 : 0 ≤ B) (hB : ∀ (k j : Fin 3), |CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => f w k) j z| ≤ B) (i m j : Fin 3) : |CKN.spatialPartial (serrinForceFlux f i m) j z| ≤ B

The spatial derivative of the antisymmetric flux is a signed first derivative of a field component.

theorem CIV.spatialPartial_serrinVortFlux_eq {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hcl : IsClassicalSolutionOn u p f unitCylinder) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ unitCylinder) (i m j : Fin 3) : CKN.spatialPartial (serrinVortFlux u f i m) j z = CKN.spatialPartial (curlComp u m) j z * u z i + curlComp u m z * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) j z - (CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w m) j z * curlComp u i z + u z m * CKN.spatialPartial (curlComp u i) j z) + CKN.spatialPartial (serrinForceFlux f i m) j z

The spatial derivative of the divergence-form flux, expanded by the product rule.

theorem CIV.sum_spatialPartial_single (g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (j : Fin 3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ∑ l : Fin 3, CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => if l = j then g w else 0) l z = CKN.spatialPartial g j z

A field supported on one index: its divergence is the partial of that component.

theorem CIV.abs_spatialPartial_force_le {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Mf : ℝ} (hMf : ∀ z ∈ unitCylinder, ∀ (i : Fin 3) (α : Fin 3 → ℕ), α 0 + α 1 + α 2 ≤ 2 → |multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => f w i) α z| ≤ Mf) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ unitCylinder) (k j : Fin 3) : |CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => f w k) j z| ≤ Mf

The first-derivative bound of the partial derivative of the force.

theorem CIV.vec3EuclideanNorm_sub_le_add (x y z : CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ CKN.Foundation.Parabolic.vec3EuclideanNorm (y - z) + CKN.Foundation.Parabolic.vec3EuclideanNorm (z - x)

The triangle inequality through an intermediate point.

theorem CIV.LS1_local_level1 : ∃ (C : ℝ), 0 < C ∧ ∀ (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3), IsClassicalSolutionOn u p f unitCylinder → ∀ (Mf Mu Ω₀ : ℝ), (∀ z ∈ unitCylinder, ∀ (i : Fin 3) (α : Fin 3 → ℕ), α 0 + α 1 + α 2 ≤ 2 → |multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => f w i) α z| ≤ Mf) → ∀ (x : CKN.Foundation.Parabolic.Vec3) (s ρ Λ : ℝ), 0 < ρ → ρ ≤ 1 → (∀ (y : CKN.Foundation.Parabolic.Vec3) (s' : ℝ), CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ 2 * ρ → s - ρ ^ 2 ≤ s' → s' ≤ s → (y, s') ∈ unitCylinder ∧ (∀ (i : Fin 3), |u (y, s') i| ≤ Mu) ∧ vortSum0 u (y, s') ≤ Ω₀ ∧ vortSum1 u (y, s') ≤ Λ) → vortSum1 u (x, s) ≤ C * (1 + Mu + Ω₀) * ρ * Λ + C * (1 + Mu + Ω₀ + Mf) ^ 2 / ρ

The local step at level one.

theorem CIV.abs_spatialSecondPartial_force_le {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Mf : ℝ} (hf : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => f z) unitCylinder) (hMf : ∀ z ∈ unitCylinder, ∀ (i : Fin 3) (α : Fin 3 → ℕ), α 0 + α 1 + α 2 ≤ 2 → |multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => f w i) α z| ≤ Mf) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ unitCylinder) (k j l : Fin 3) : |CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial (fun (w' : CKN.Foundation.Parabolic.ParabolicPoint) => f w' k) j w) l z| ≤ Mf

The second-derivative bound of the force, in any order of the two partials.

theorem CIV.abs_spatialPartial2_curlComp_le_vortSum2 (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j l : Fin 3) : |CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial (curlComp u i) j w) l z| ≤ vortSum2 u z

Each second derivative of the vorticity is bounded by the level-two sum.

theorem CIV.abs_spatialPartial2_le_velSum2 (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j l : Fin 3) : |CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial (fun (w' : CKN.Foundation.Parabolic.ParabolicPoint) => u w' i) j w) l z| ≤ velSum2 u z

Each second derivative of the velocity is bounded by the level-two velocity sum.

theorem CIV.abs_spatialPartial2_serrinForceFlux_le {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Mf : ℝ} (hf : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => f z) unitCylinder) (hMf : ∀ z ∈ unitCylinder, ∀ (i : Fin 3) (α : Fin 3 → ℕ), α 0 + α 1 + α 2 ≤ 2 → |multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => f w i) α z| ≤ Mf) (hMf0 : 0 ≤ Mf) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ unitCylinder) (i m j l : Fin 3) : |CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial (serrinForceFlux f i m) j w) l z| ≤ Mf

The second derivative of the antisymmetric flux of the force is bounded by Mf.

theorem CIV.abs_spatialPartial2_serrinVortFlux_le {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hcl : IsClassicalSolutionOn u p f unitCylinder) {Mf : ℝ} (hMf : ∀ z ∈ unitCylinder, ∀ (i : Fin 3) (α : Fin 3 → ℕ), α 0 + α 1 + α 2 ≤ 2 → |multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => f w i) α z| ≤ Mf) (hMf0 : 0 ≤ Mf) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ unitCylinder) {Mu Ω₀ Ω₁ V₁ L₂ V₂ : ℝ} (hu : ∀ (k : Fin 3), |u z k| ≤ Mu) (hω0 : ∀ (k : Fin 3), |curlComp u k z| ≤ Ω₀) (hω1 : ∀ (k a : Fin 3), |CKN.spatialPartial (curlComp u k) a z| ≤ Ω₁) (hv1 : ∀ (k a : Fin 3), |CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w k) a z| ≤ V₁) (hω2 : ∀ (k a b : Fin 3), |CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial (curlComp u k) a w) b z| ≤ L₂) (hv2 : ∀ (k a b : Fin 3), |CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial (fun (w' : CKN.Foundation.Parabolic.ParabolicPoint) => u w' k) a w) b z| ≤ V₂) (i m j l : Fin 3) : |CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial (serrinVortFlux u f i m) j w) l z| ≤ 2 * Mu * L₂ + 4 * Ω₁ * V₁ + 2 * Ω₀ * V₂ + Mf

Bound for the second spatial derivative of the divergence-form flux.

theorem CIV.LS2_local_level2 : ∃ (C : ℝ), 0 < C ∧ ∀ (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3), IsClassicalSolutionOn u p f unitCylinder → ∀ (Mf Mu Ω₀ Ω₁ V₁ : ℝ), (∀ z ∈ unitCylinder, ∀ (i : Fin 3) (α : Fin 3 → ℕ), α 0 + α 1 + α 2 ≤ 2 → |multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => f w i) α z| ≤ Mf) → ∀ (x : CKN.Foundation.Parabolic.Vec3) (s ρ Λ : ℝ), 0 < ρ → ρ ≤ 1 → (∀ (y : CKN.Foundation.Parabolic.Vec3) (s' : ℝ), CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ 2 * ρ → s - ρ ^ 2 ≤ s' → s' ≤ s → (y, s') ∈ unitCylinder ∧ (∀ (i : Fin 3), |u (y, s') i| ≤ Mu) ∧ vortSum0 u (y, s') ≤ Ω₀ ∧ vortSum1 u (y, s') ≤ Ω₁ ∧ velSum1 u (y, s') ≤ V₁ ∧ vortSum2 u (y, s') ≤ Λ) → vortSum2 u (x, s) ≤ C * (1 + Mu + Ω₀) * ρ * Λ + C * (1 + Mu + Ω₀ + Ω₁ + V₁ + Mf) ^ 2 / ρ

The local step at level two.