The fourth-power bound for the velocity gradient

A bounded velocity whose gradient and second derivatives are square integrable has a gradient in L⁴ on a smaller box, with the bound of lem:vorticity-products (the H² product estimate): the smooth interpolation inequality applied at every time to backward mollifications, integrated in time, and passed to the limit by Fatou's lemma.

theorem ESS.vorticity_spatialDeriv_congr_on {f g : CKN.Foundation.Parabolic.Vec3 → ℝ} {U : Set CKN.Foundation.Parabolic.Vec3} (hU : IsOpen U) (hfg : ∀ x ∈ U, f x = g x) {x : CKN.Foundation.Parabolic.Vec3} (hx : x ∈ U) (j : Fin 3) : CKN.spatialDeriv f j x = CKN.spatialDeriv g j x

Coordinate derivatives of functions agreeing on an open set agree there.

theorem ESS.vorticity_indicator_bound {W : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hW : MeasurableSet W) {f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {M : ℝ} (hM : 0 ≤ M) (hf : ∀ᵐ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) ∂MeasureTheory.volume.restrict W, |f z| ≤ M) : ∀ᵐ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), |W.indicator f z| ≤ M

An almost-everywhere bound on a set bounds the zero extension.

theorem ESS.vorticity_sq_sum_three_le (A : Fin 3 → ℝ) : (∑ i : Fin 3, A i) ^ 2 ≤ 3 * ∑ i : Fin 3, A i ^ 2

The square of a sum of three nonnegative terms is at most three times the sum of squares.

theorem ESS.vorticityLevelTwo_L4 (M K₀ K₂ : ℝ) (hM : 0 ≤ M) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (x₀ : CKN.Foundation.Parabolic.Vec3) (a t₀ : ℝ) (U : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (G : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (D2 : Fin 3 → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), (∀ (i : Fin 3), MeasureTheory.MemLp (U i) 2 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ (14 / 16) ×ˢ Set.Ioo a t₀))) → (∀ᵐ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) ∂MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ (14 / 16) ×ˢ Set.Ioo a t₀), ∀ (i : Fin 3), |U i z| ≤ M) → (∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) 2 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ (14 / 16) ×ˢ Set.Ioo a t₀))) → ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (14 / 16) ×ˢ Set.Ioo a t₀, ∑ i : Fin 3, ∑ j : Fin 3, G i j z ^ 2 ≤ K₀ → (∀ (i j k : Fin 3), MeasureTheory.MemLp (D2 i j k) 2 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ (14 / 16) ×ˢ Set.Ioo a t₀))) → ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (14 / 16) ×ˢ Set.Ioo a t₀, ∑ i : Fin 3, ∑ j : Fin 3, ∑ k : Fin 3, D2 i j k z ^ 2 ≤ K₂ → (∀ (i j : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ CKN.Foundation.Parabolic.vec3Ball x₀ (14 / 16) ×ˢ Set.Ioo a t₀ → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (14 / 16) ×ˢ Set.Ioo a t₀, U i y * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (14 / 16) ×ˢ Set.Ioo a t₀, G i j y * ψ y) → (∀ (i j k : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ CKN.Foundation.Parabolic.vec3Ball x₀ (14 / 16) ×ˢ Set.Ioo a t₀ → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (14 / 16) ×ˢ Set.Ioo a t₀, G i j y * CKN.spatialPartial ψ k y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (14 / 16) ×ˢ Set.Ioo a t₀, D2 i j k y * ψ y) → MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => (∑ i : Fin 3, ∑ j : Fin 3, G i j z ^ 2) ^ 2) (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ (13 / 16) ×ˢ Set.Ioo (a + 1 / 16) t₀)) ∧ ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (13 / 16) ×ˢ Set.Ioo (a + 1 / 16) t₀, (∑ i : Fin 3, ∑ j : Fin 3, G i j z ^ 2) ^ 2 ≤ K

The fourth-power bound for the velocity gradient on a smaller box (the H² product estimate of lem:vorticity-products, localized).