The first level of the vorticity bootstrap

From the starting data on the unit box, the weak local heat gain gives square-integrable first spatial derivatives of the vorticity, and the weak div–curl recovery gives square-integrable second spatial derivatives of the velocity, with bounds by the velocity bound and the gradient energy (the initial energy level and the first velocity level of thm:vorticity-regularity).

theorem ESS.vorticityCurl_memLp {μ : MeasureTheory.Measure (CKN.Foundation.Parabolic.Vec3 × ℝ)} {G : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hG : ∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) 2 μ) (l : Fin 3) : MeasureTheory.MemLp (vorticityCurl G l) 2 μ

The vorticity components of a square-integrable gradient are square integrable.

theorem ESS.vorticityFluxOf_memLp {μ : MeasureTheory.Measure (CKN.Foundation.Parabolic.Vec3 × ℝ)} {U : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {G : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {M : ℝ} (hU : ∀ (i : Fin 3), MeasureTheory.AEStronglyMeasurable (U i) μ) (hG : ∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) 2 μ) (hUb : ∀ᵐ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) ∂μ, ∀ (i : Fin 3), |U i z| ≤ M) (i j : Fin 3) : MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => -(U j z * vorticityCurl G i z - vorticityCurl G j z * U i z)) 2 μ

The vorticity flux of a bounded velocity and a square-integrable gradient.

theorem ESS.vorticityFluxOf_sq_le {U : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {G : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {M : ℝ} {z : CKN.Foundation.Parabolic.Vec3 × ℝ} (hz : ∀ (i : Fin 3), |U i z| ≤ M) (i : Fin 3) : vorticityCurl G i z ^ 2 + ∑ j : Fin 3, (-(U j z * vorticityCurl G i z - vorticityCurl G j z * U i z)) ^ 2 ≤ (2 + 24 * M ^ 2) * ∑ a : Fin 3, ∑ b : Fin 3, G a b z ^ 2

The pointwise bound of the vorticity and its flux by the gradient.

theorem ESS.vorticityLevelOne_heat (M K₀ : ℝ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ : ℝ) (U : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (G : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), (∀ (i : Fin 3), MeasureTheory.MemLp (U i) 2 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ 1 ×ˢ Set.Ioo (t₀ - 1) t₀))) → (∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) 2 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ 1 ×ˢ Set.Ioo (t₀ - 1) t₀))) → (∀ᵐ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) ∂MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ 1 ×ˢ Set.Ioo (t₀ - 1) t₀), ∀ (i : Fin 3), |U i z| ≤ M) → ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ 1 ×ˢ Set.Ioo (t₀ - 1) t₀, ∑ i : Fin 3, ∑ j : Fin 3, G i j z ^ 2 ≤ K₀ → (∀ (i : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ CKN.Foundation.Parabolic.vec3Ball x₀ 1 ×ˢ Set.Ioo (t₀ - 1) t₀ → ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ 1 ×ˢ Set.Ioo (t₀ - 1) t₀, vorticityCurl G i z * (-CKN.timePartial ψ z - ∑ j : Fin 3, CKN.spatialSecondPartial ψ j j z) = -∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ 1 ×ˢ Set.Ioo (t₀ - 1) t₀, ∑ j : Fin 3, -(U j z * vorticityCurl G i z - vorticityCurl G j z * U i z) * CKN.spatialPartial ψ j z) → ∃ (Ω1 : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), (∀ (i j : Fin 3), MeasureTheory.MemLp (Ω1 i j) 2 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ (15 / 16) ×ˢ Set.Ioo (t₀ - 1 + 1 / 16) t₀))) ∧ (∀ (i j : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ CKN.Foundation.Parabolic.vec3Ball x₀ (15 / 16) ×ˢ Set.Ioo (t₀ - 1 + 1 / 16) t₀ → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (15 / 16) ×ˢ Set.Ioo (t₀ - 1 + 1 / 16) t₀, vorticityCurl G i y * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (15 / 16) ×ˢ Set.Ioo (t₀ - 1 + 1 / 16) t₀, Ω1 i j y * ψ y) ∧ ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (15 / 16) ×ˢ Set.Ioo (t₀ - 1 + 1 / 16) t₀, ∑ i : Fin 3, ∑ j : Fin 3, Ω1 i j y ^ 2 ≤ K

The heat step of the first level: square-integrable first derivatives of the vorticity (the initial energy level of thm:vorticity-regularity).

theorem ESS.vorticityAntisym_memLp {μ : MeasureTheory.Measure (CKN.Foundation.Parabolic.Vec3 × ℝ)} {v : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hv : ∀ (l : Fin 3), MeasureTheory.MemLp (v l) 2 μ) (i k : Fin 3) : MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => vorticityAntisym (fun (l : Fin 3) => v l z) i k) 2 μ

The antisymmetric matrix of square-integrable fields is square integrable.

theorem ESS.vorticityLevelOne_divCurl (K₀ K₁ : ℝ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ : ℝ) (U : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (G Ω1 : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), (∀ (i : Fin 3), MeasureTheory.MemLp (U i) 2 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ 1 ×ˢ Set.Ioo (t₀ - 1) t₀))) → (∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) 2 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ 1 ×ˢ Set.Ioo (t₀ - 1) t₀))) → ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ 1 ×ˢ Set.Ioo (t₀ - 1) t₀, ∑ i : Fin 3, ∑ j : Fin 3, G i j z ^ 2 ≤ K₀ → (∀ (i j : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ CKN.Foundation.Parabolic.vec3Ball x₀ 1 ×ˢ Set.Ioo (t₀ - 1) t₀ → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ 1 ×ˢ Set.Ioo (t₀ - 1) t₀, U i y * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ 1 ×ˢ Set.Ioo (t₀ - 1) t₀, G i j y * ψ y) → (∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ CKN.Foundation.Parabolic.vec3Ball x₀ 1 ×ˢ Set.Ioo (t₀ - 1) t₀ → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ 1 ×ˢ Set.Ioo (t₀ - 1) t₀, ∑ i : Fin 3, U i y * CKN.spatialPartial ψ i y = 0) → (∀ (i j : Fin 3), MeasureTheory.MemLp (Ω1 i j) 2 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ (15 / 16) ×ˢ Set.Ioo (t₀ - 1 + 1 / 16) t₀))) → (∀ (i j : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ CKN.Foundation.Parabolic.vec3Ball x₀ (15 / 16) ×ˢ Set.Ioo (t₀ - 1 + 1 / 16) t₀ → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (15 / 16) ×ˢ Set.Ioo (t₀ - 1 + 1 / 16) t₀, vorticityCurl G i y * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (15 / 16) ×ˢ Set.Ioo (t₀ - 1 + 1 / 16) t₀, Ω1 i j y * ψ y) → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (15 / 16) ×ˢ Set.Ioo (t₀ - 1 + 1 / 16) t₀, ∑ i : Fin 3, ∑ j : Fin 3, Ω1 i j y ^ 2 ≤ K₁ → ∃ (D2 : Fin 3 → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), (∀ (i j k : Fin 3), MeasureTheory.MemLp (D2 i j k) 2 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ (14 / 16) ×ˢ Set.Ioo (t₀ - 1 + 1 / 16 + 1 / 16) t₀))) ∧ (∀ (i j k : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ CKN.Foundation.Parabolic.vec3Ball x₀ (14 / 16) ×ˢ Set.Ioo (t₀ - 1 + 1 / 16 + 1 / 16) t₀ → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (14 / 16) ×ˢ Set.Ioo (t₀ - 1 + 1 / 16 + 1 / 16) t₀, G i j y * CKN.spatialPartial ψ k y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (14 / 16) ×ˢ Set.Ioo (t₀ - 1 + 1 / 16 + 1 / 16) t₀, D2 i j k y * ψ y) ∧ ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (14 / 16) ×ˢ Set.Ioo (t₀ - 1 + 1 / 16 + 1 / 16) t₀, ∑ i : Fin 3, ∑ j : Fin 3, ∑ k : Fin 3, D2 i j k y ^ 2 ≤ K

The div–curl step of the first level: square-integrable second derivatives of the velocity (the first velocity level of thm:vorticity-regularity).