The level bounds of the interior estimates

On an annular cylinder {a < |x| < b} × (t₁, 0) inside the unit cylinder where the velocity is bounded, the vorticity and its first two spatial derivatives are bounded on every smaller annular cylinder, uniformly up to the top time t = 0. Each level is the weighted absorption applied to the corresponding local step. These are the level bounds of the interior estimates in the proof of lem:aniso:annulus.

theorem CIV.level_bound_of_local {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {a b t₁ c₁ c₂ : ℝ} (hab : 0 ≤ a ∧ a < b ∧ b < 1) (ht₁ : -1 < t₁ ∧ t₁ < 0) (hc₁ : 0 ≤ c₁) (hc₂ : 0 ≤ c₂) (hg0 : ∀ (z : CKN.Foundation.Parabolic.ParabolicPoint), 0 ≤ g z) (hgc : ContinuousOn (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) unitCylinder) (hstep : ∀ (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 → a < CKN.Foundation.Parabolic.vec3EuclideanNorm y ∧ CKN.Foundation.Parabolic.vec3EuclideanNorm y < b ∧ t₁ < s' ∧ s' < 0 ∧ g (y, s') ≤ Λ) → g (x, s) ≤ c₁ * ρ * Λ + c₂ / ρ) {a' b' t₁' : ℝ} (hab' : a < a' ∧ a' < b' ∧ b' < b) (ht₁' : t₁ < t₁' ∧ t₁' < 0) : ∃ (K : ℝ), ∀ (x : CKN.Foundation.Parabolic.Vec3), a' < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < b' → ∀ s ∈ Set.Ioo t₁' 0, g (x, s) ≤ K

The absorption step shared by the three levels: a nonnegative level function, continuous on the unit cylinder, that satisfies a local circular estimate on backward windows inside the annular cylinder is bounded on every smaller annular cylinder.

theorem CIV.mem_unitCylinder_of_annulus {b t₁ : ℝ} (hb1 : b < 1) (ht₁ : -1 < t₁) {y : CKN.Foundation.Parabolic.Vec3} {s : ℝ} (hy : CKN.Foundation.Parabolic.vec3EuclideanNorm y < b) (hs : t₁ < s) (hs0 : s < 0) : (y, s) ∈ unitCylinder

A point of the annular cylinder lies in the unit cylinder.

theorem CIV.LV0_level0 {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) {a b t₁ Mu : ℝ} (hab : 0 ≤ a ∧ a < b ∧ b < 1) (ht₁ : -1 < t₁ ∧ t₁ < 0) (hu : ∀ (x : CKN.Foundation.Parabolic.Vec3), a < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < b → ∀ s ∈ Set.Ioo t₁ 0, ∀ (i : Fin 3), |u (x, s) i| ≤ Mu) {a' b' t₁' : ℝ} (hab' : a < a' ∧ a' < b' ∧ b' < b) (ht₁' : t₁ < t₁' ∧ t₁' < 0) : ∃ (K : ℝ), ∀ (x : CKN.Foundation.Parabolic.Vec3), a' < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < b' → ∀ s ∈ Set.Ioo t₁' 0, vortSum0 u (x, s) ≤ K

Level zero: the vorticity is bounded on every smaller annular cylinder.

theorem CIV.LV1_level1 {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) {a b t₁ Mu Ω₀ : ℝ} (hab : 0 ≤ a ∧ a < b ∧ b < 1) (ht₁ : -1 < t₁ ∧ t₁ < 0) (hu : ∀ (x : CKN.Foundation.Parabolic.Vec3), a < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < b → ∀ s ∈ Set.Ioo t₁ 0, ∀ (i : Fin 3), |u (x, s) i| ≤ Mu) (hω₀ : ∀ (x : CKN.Foundation.Parabolic.Vec3), a < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < b → ∀ s ∈ Set.Ioo t₁ 0, vortSum0 u (x, s) ≤ Ω₀) {a' b' t₁' : ℝ} (hab' : a < a' ∧ a' < b' ∧ b' < b) (ht₁' : t₁ < t₁' ∧ t₁' < 0) : ∃ (K : ℝ), ∀ (x : CKN.Foundation.Parabolic.Vec3), a' < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < b' → ∀ s ∈ Set.Ioo t₁' 0, vortSum1 u (x, s) ≤ K

Level one: the first spatial derivatives of the vorticity are bounded on every smaller annular cylinder.

theorem CIV.LV2_level2 {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) {a b t₁ Mu Ω₀ Ω₁ V₁ : ℝ} (hab : 0 ≤ a ∧ a < b ∧ b < 1) (ht₁ : -1 < t₁ ∧ t₁ < 0) (hu : ∀ (x : CKN.Foundation.Parabolic.Vec3), a < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < b → ∀ s ∈ Set.Ioo t₁ 0, ∀ (i : Fin 3), |u (x, s) i| ≤ Mu) (hω₀ : ∀ (x : CKN.Foundation.Parabolic.Vec3), a < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < b → ∀ s ∈ Set.Ioo t₁ 0, vortSum0 u (x, s) ≤ Ω₀) (hω₁ : ∀ (x : CKN.Foundation.Parabolic.Vec3), a < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < b → ∀ s ∈ Set.Ioo t₁ 0, vortSum1 u (x, s) ≤ Ω₁) (hv₁ : ∀ (x : CKN.Foundation.Parabolic.Vec3), a < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < b → ∀ s ∈ Set.Ioo t₁ 0, velSum1 u (x, s) ≤ V₁) {a' b' t₁' : ℝ} (hab' : a < a' ∧ a' < b' ∧ b' < b) (ht₁' : t₁ < t₁' ∧ t₁' < 0) : ∃ (K : ℝ), ∀ (x : CKN.Foundation.Parabolic.Vec3), a' < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < b' → ∀ s ∈ Set.Ioo t₁' 0, vortSum2 u (x, s) ≤ K

Level two: the second spatial derivatives of the vorticity are bounded on every smaller annular cylinder.