Local elliptic bounds on a time slice

For a divergence-free velocity u smooth near the closed Euclidean ball |y - x| ≤ ρ of one time slice, the velocity gradient and Hessian at the centre are controlled by the vorticity gradient and Hessian on the ball and by the velocity itself: ∑ᵢⱼ |∂ⱼuᵢ(x)| ≤ C (ρ Λ₁ + M / ρ) (EL1_local) and ∑ᵢⱼₗ |∂ₗ∂ⱼuᵢ(x)| ≤ C (ρ Λ₂ + M / ρ²) (EL2_local), with an absolute constant C.

The proof applies the Newtonian representation ∂ₗv(x) = -∫ ∂ₗN(x - y) Δv(y) dy to v = χ uᵢ (respectively v = χ ∂ⱼuᵢ), where χ is the ball cutoff, after replacing u by a globally smooth field that agrees with it near the ball. The Leibniz rule splits Δv into χ Δh, which is bounded through Δuᵢ = ∑ₖ ∂ₖ(∂ₖuᵢ - ∂ᵢuₖ) (divergence free) and the signed vorticity form of the antisymmetric gradient, against ∫_{B_ρ} |∂ₗN| ≤ Cρ; and the cutoff terms ∂ₖχ ∂ₖh and ∂ₖ∂ₖχ h, which are bounded by the annular kernel bound using only |u| ≤ M. The level bounds EV1_velocity_gradient and EV2_velocity_hessian apply these at the fixed radius min (a' - a, b - b', 1) / 2 on an annulus times a backward time interval. These are the elliptic steps of the interior estimates in the proof of lem:aniso:annulus.

Part 1: a smooth extension of one time slice

Part 2: calculus of spatialDeriv for smooth functions

Part 3: the Newtonian representation split along the cutoff

Part 4: the annular cutoff terms, through the annular kernel bound

Part 5: the Laplacian of a divergence-free field through its curl

Part 6: the pointwise bounds for a smooth divergence-free field

Part 7: transfer from the velocity to its smooth extension

Part 8: the local elliptic bounds EL1 and EL2

theorem CIV.EL1_local : ∃ (C : ℝ), 0 < C ∧ ∀ (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (O : Set CKN.Foundation.Parabolic.ParabolicPoint) (x : CKN.Foundation.Parabolic.Vec3) (t ρ M Λ : ℝ), IsOpen O → 0 < ρ → ρ ≤ 1 → (∀ (y : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ → (y, t) ∈ O) → ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) O → (∀ z ∈ O, ∑ j : Fin 3, CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w j) j z = 0) → (∀ (y : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ → ∀ (i : Fin 3), |u (y, t) i| ≤ M) → (∀ (y : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ → vortSum1 u (y, t) ≤ Λ) → velSum1 u (x, t) ≤ C * (ρ * Λ + M / ρ)

First-order local elliptic bound on a time slice: for a divergence-free velocity smooth near the closed ball |y - x| ≤ ρ of the slice t, the velocity gradient at the centre is bounded by C (ρ Λ + M / ρ), where M bounds the velocity and Λ the vorticity gradient on the ball.

theorem CIV.EL2_local : ∃ (C : ℝ), 0 < C ∧ ∀ (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (O : Set CKN.Foundation.Parabolic.ParabolicPoint) (x : CKN.Foundation.Parabolic.Vec3) (t ρ M Λ : ℝ), IsOpen O → 0 < ρ → ρ ≤ 1 → (∀ (y : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ → (y, t) ∈ O) → ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) O → (∀ z ∈ O, ∑ j : Fin 3, CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w j) j z = 0) → (∀ (y : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ → ∀ (i : Fin 3), |u (y, t) i| ≤ M) → (∀ (y : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ → vortSum2 u (y, t) ≤ Λ) → velSum2 u (x, t) ≤ C * (ρ * Λ + M / ρ ^ 2)

Second-order local elliptic bound on a time slice: for a divergence-free velocity smooth near the closed ball |y - x| ≤ ρ of the slice t, the velocity Hessian at the centre is bounded by C (ρ Λ + M / ρ²), where M bounds the velocity and Λ the vorticity Hessian on the ball.

Part 9: the velocity level bounds EV1 and EV2

theorem CIV.EV1_velocity_gradient {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) {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, vortSum1 u (x, s) ≤ Ω₁) {a' b' : ℝ} (hab' : a < a' ∧ a' < b' ∧ b' < b) : ∃ (K : ℝ), ∀ (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) ≤ K

Velocity-gradient level bound: a bound on the vorticity gradient over an annulus times a backward time interval gives a bound on the velocity gradient over any inner annulus.

theorem CIV.EV2_velocity_hessian {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) {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, vortSum2 u (x, s) ≤ Ω₂) {a' b' : ℝ} (hab' : a < a' ∧ a' < b' ∧ b' < b) : ∃ (K : ℝ), ∀ (x : CKN.Foundation.Parabolic.Vec3), a' < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < b' → ∀ s ∈ Set.Ioo t₁ 0, velSum2 u (x, s) ≤ K

Velocity-Hessian level bound: a bound on the vorticity Hessian over an annulus times a backward time interval gives a bound on the velocity Hessian over any inner annulus.