One spatial derivative more for the velocity and the pressure

The heat gradient bound applied to ∂^α uᵢ, whose heat residual is ∂^α of the forced Navier–Stokes right-hand side, and the Laplace gradient bound applied to the time slice of ∂^α p, whose Laplacian is ∂^α (div f − ∑ᵢⱼ ∂ᵢuⱼ ∂ⱼuᵢ), bound every derivative of order k + 1 by ρ times the order-k source and 1/ρ times the order-k field. The products are bounded with the multi-index Leibniz rule. This is the one-step estimate of the induction in the proof of thm:analytic:interior.

theorem CIV.exists_eq_add_single_of_order_succ {β : Fin 3 → ℕ} {k : ℕ} (hβ : β 0 + β 1 + β 2 = k + 1) : ∃ (l : Fin 3) (α : Fin 3 → ℕ), β = α + Pi.single l 1 ∧ α 0 + α 1 + α 2 = k

A multi-index of order k + 1 is a multi-index of order k plus one unit direction.

theorem CIV.order_add_single (α : Fin 3 → ℕ) (l : Fin 3) : (α + Pi.single l 1) 0 + (α + Pi.single l 1) 1 + (α + Pi.single l 1) 2 = α 0 + α 1 + α 2 + 1

Adding one unit direction raises the order by one.

theorem CIV.kahane_velocity_step : ∃ (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) (Ω : Set CKN.Foundation.Parabolic.Vec3) (I : Set ℝ), IsOpen Ω → IsOpen I → IsClassicalSolutionOn u p f (CKN.spaceTimeSet Ω I) → ∀ (x : CKN.Foundation.Parabolic.Vec3) (t ρ : ℝ) (k : ℕ) (c : ℕ → ℝ) (P F : ℝ), 0 < ρ → ρ ≤ 1 → {y : CKN.Foundation.Parabolic.Vec3 | CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ} ×ˢ Set.Icc (t - ρ ^ 2) t ⊆ CKN.spaceTimeSet Ω I → (∀ z ∈ {y : CKN.Foundation.Parabolic.Vec3 | CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ} ×ˢ Set.Icc (t - ρ ^ 2) t, ∀ (γ : Fin 3 → ℕ), γ 0 + γ 1 + γ 2 ≤ k + 1 → ∀ (j : Fin 3), |multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w j) γ z| ≤ c (γ 0 + γ 1 + γ 2)) → (∀ z ∈ {y : CKN.Foundation.Parabolic.Vec3 | CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ} ×ˢ Set.Icc (t - ρ ^ 2) t, ∀ (γ : Fin 3 → ℕ), γ 0 + γ 1 + γ 2 = k + 1 → |multiPartial p γ z| ≤ P) → (∀ z ∈ {y : CKN.Foundation.Parabolic.Vec3 | CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ} ×ˢ Set.Icc (t - ρ ^ 2) t, ∀ (γ : Fin 3 → ℕ), γ 0 + γ 1 + γ 2 = k → ∀ (i : Fin 3), |multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => f w i) γ z| ≤ F) → ∀ (β : Fin 3 → ℕ), β 0 + β 1 + β 2 = k + 1 → ∀ (i : Fin 3), |multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) β (x, t)| ≤ C * (ρ * (F + 3 * ∑ m ∈ Finset.range (k + 1), ↑(k.choose m) * (c m * c (k + 1 - m)) + P) + c k / ρ)

One spatial derivative more for the velocity: with window bounds c m on the velocity derivatives of order m ≤ k + 1, P on the pressure derivatives of order k + 1 and F on the force derivatives of order k, every velocity derivative of order k + 1 at the top of the window is at most C (ρ (F + 3 ∑ₘ C(k,m) c m c (k+1-m) + P) + c k / ρ).

theorem CIV.kahane_pressure_step : ∃ (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) (Ω : Set CKN.Foundation.Parabolic.Vec3) (I : Set ℝ), IsOpen Ω → IsOpen I → IsClassicalSolutionOn u p f (CKN.spaceTimeSet Ω I) → ∀ (x : CKN.Foundation.Parabolic.Vec3) (t ρ : ℝ) (k : ℕ) (c : ℕ → ℝ) (Q F : ℝ), 0 < ρ → ρ ≤ 1 → t ∈ I → (∀ (y : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ → y ∈ Ω) → (∀ (y : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ → ∀ (γ : Fin 3 → ℕ), γ 0 + γ 1 + γ 2 ≤ k + 1 → ∀ (j : Fin 3), |multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w j) γ (y, t)| ≤ c (γ 0 + γ 1 + γ 2)) → (∀ (y : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ → ∀ (γ : Fin 3 → ℕ), γ 0 + γ 1 + γ 2 = k → |multiPartial p γ (y, t)| ≤ Q) → (∀ (y : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ → ∀ (γ : Fin 3 → ℕ), γ 0 + γ 1 + γ 2 = k + 1 → ∀ (i : Fin 3), |multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => f w i) γ (y, t)| ≤ F) → ∀ (β : Fin 3 → ℕ), β 0 + β 1 + β 2 = k + 1 → |multiPartial p β (x, t)| ≤ C * (ρ * (3 * F + 9 * ∑ m ∈ Finset.range (k + 1), ↑(k.choose m) * (c (m + 1) * c (k + 1 - m))) + Q / ρ)

One spatial derivative more for the pressure: with bounds c m on the velocity derivatives of order m ≤ k + 1 on the time slice of B_bar(x, ρ), Q on the pressure derivatives of order k and F on the force derivatives of order k + 1 there, every pressure derivative of order k + 1 at x is at most C (ρ (3 F + 9 ∑ₘ C(k,m) c (m+1) c (k+1-m)) + Q / ρ).

theorem CIV.kahane_velocity_pressure_step : ∃ (C : ℝ), 1 ≤ C ∧ (∀ (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Ω : Set CKN.Foundation.Parabolic.Vec3) (I : Set ℝ), IsOpen Ω → IsOpen I → IsClassicalSolutionOn u p f (CKN.spaceTimeSet Ω I) → ∀ (x : CKN.Foundation.Parabolic.Vec3) (t ρ : ℝ) (k : ℕ) (c : ℕ → ℝ) (P F : ℝ), 0 < ρ → ρ ≤ 1 → {y : CKN.Foundation.Parabolic.Vec3 | CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ} ×ˢ Set.Icc (t - ρ ^ 2) t ⊆ CKN.spaceTimeSet Ω I → (∀ z ∈ {y : CKN.Foundation.Parabolic.Vec3 | CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ} ×ˢ Set.Icc (t - ρ ^ 2) t, ∀ (γ : Fin 3 → ℕ), γ 0 + γ 1 + γ 2 ≤ k + 1 → ∀ (j : Fin 3), |multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w j) γ z| ≤ c (γ 0 + γ 1 + γ 2)) → (∀ z ∈ {y : CKN.Foundation.Parabolic.Vec3 | CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ} ×ˢ Set.Icc (t - ρ ^ 2) t, ∀ (γ : Fin 3 → ℕ), γ 0 + γ 1 + γ 2 = k + 1 → |multiPartial p γ z| ≤ P) → (∀ z ∈ {y : CKN.Foundation.Parabolic.Vec3 | CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ} ×ˢ Set.Icc (t - ρ ^ 2) t, ∀ (γ : Fin 3 → ℕ), γ 0 + γ 1 + γ 2 = k → ∀ (i : Fin 3), |multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => f w i) γ z| ≤ F) → ∀ (β : Fin 3 → ℕ), β 0 + β 1 + β 2 = k + 1 → ∀ (i : Fin 3), |multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) β (x, t)| ≤ C * (ρ * (F + 3 * ∑ m ∈ Finset.range (k + 1), ↑(k.choose m) * (c m * c (k + 1 - m)) + P) + c k / ρ)) ∧ ∀ (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Ω : Set CKN.Foundation.Parabolic.Vec3) (I : Set ℝ), IsOpen Ω → IsOpen I → IsClassicalSolutionOn u p f (CKN.spaceTimeSet Ω I) → ∀ (x : CKN.Foundation.Parabolic.Vec3) (t ρ : ℝ) (k : ℕ) (c : ℕ → ℝ) (Q F : ℝ), 0 < ρ → ρ ≤ 1 → t ∈ I → (∀ (y : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ → y ∈ Ω) → (∀ (y : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ → ∀ (γ : Fin 3 → ℕ), γ 0 + γ 1 + γ 2 ≤ k + 1 → ∀ (j : Fin 3), |multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w j) γ (y, t)| ≤ c (γ 0 + γ 1 + γ 2)) → (∀ (y : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ → ∀ (γ : Fin 3 → ℕ), γ 0 + γ 1 + γ 2 = k → |multiPartial p γ (y, t)| ≤ Q) → (∀ (y : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ → ∀ (γ : Fin 3 → ℕ), γ 0 + γ 1 + γ 2 = k + 1 → ∀ (i : Fin 3), |multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => f w i) γ (y, t)| ≤ F) → ∀ (β : Fin 3 → ℕ), β 0 + β 1 + β 2 = k + 1 → |multiPartial p β (x, t)| ≤ C * (ρ * (3 * F + 9 * ∑ m ∈ Finset.range (k + 1), ↑(k.choose m) * (c (m + 1) * c (k + 1 - m))) + Q / ρ)

The velocity and pressure steps with one common constant C ≥ 1.