The continuous representative of the vorticity #
A field solving a heat equation with square-integrable flux, whose first and second spatial
weak derivatives solve heat equations of the same kind, has a representative which is continuous
and bounded up to the top time on a smaller closed box: at every time the backward mollifications
are Cauchy in the uniform norm, by the H² embedding and the uniform-in-time L² Cauchy property
of the mollified fields (the continuity statement of thm:vorticity-regularity).
theorem
ESS.vorticity_continuousRep
(Kw K1 K2 : ℝ)
:
∃ (C : ℝ),
0 ≤ C ∧ ∀ (x₀ : CKN.Foundation.Parabolic.Vec3) (a t₀ : ℝ) (w : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ)
(g Fw : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ)
(h Fg : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ)
(Fh : Fin 3 → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
a + 1 / 64 < t₀ →
t₀ ≤ a + 1 →
MeasureTheory.MemLp w 2
(MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀)) →
(∀ (m : Fin 3),
MeasureTheory.MemLp (g m) 2
(MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀))) →
(∀ (m k : Fin 3),
MeasureTheory.MemLp (h m k) 2
(MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀))) →
(∀ (j : Fin 3),
MeasureTheory.MemLp (Fw j) 2
(MeasureTheory.volume.restrict
(CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀))) →
(∀ (m j : Fin 3),
MeasureTheory.MemLp (Fg m j) 2
(MeasureTheory.volume.restrict
(CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀))) →
(∀ (m k j : Fin 3),
MeasureTheory.MemLp (Fh m k j) 2
(MeasureTheory.volume.restrict
(CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀))) →
(∀ (j : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆ CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀ →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀, w y * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀, g j y * ψ y) →
(∀ (m k : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆ CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀ →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀, g m y * CKN.spatialPartial ψ k y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀, h m k y * ψ y) →
(∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆ CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀ →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀, w y * (-CKN.timePartial ψ y - ∑ j : Fin 3, CKN.spatialSecondPartial ψ j j y) = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀, ∑ j : Fin 3, Fw j y * CKN.spatialPartial ψ j y) →
(∀ (m : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆ CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀ →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀, g m y * (-CKN.timePartial ψ y - ∑ j : Fin 3, CKN.spatialSecondPartial ψ j j y) = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀, ∑ j : Fin 3, Fg m j y * CKN.spatialPartial ψ j y) →
(∀ (m k : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆ CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀ →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀, h m k y * (-CKN.timePartial ψ y - ∑ j : Fin 3, CKN.spatialSecondPartial ψ j j y) = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀, ∑ j : Fin 3, Fh m k j y * CKN.spatialPartial ψ j y) →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀, w y ^ 2 + ∑ j : Fin 3, Fw j y ^ 2 ≤ Kw →
(∀ (m : Fin 3),
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀, g m y ^ 2 + ∑ j : Fin 3, Fg m j y ^ 2 ≤ K1) →
(∀ (m k : Fin 3),
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀, h m k y ^ 2 + ∑ j : Fin 3, Fh m k j y ^ 2 ≤ K2) →
∃ (ω : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContinuousOn ω
({x : CKN.Foundation.Parabolic.Vec3 | CKN.Foundation.Parabolic.vec3EuclideanNorm (x - x₀) ≤ 38 / 64} ×ˢ Set.Icc (a + 1 / 64) t₀) ∧ (∀
z ∈
{x : CKN.Foundation.Parabolic.Vec3 | CKN.Foundation.Parabolic.vec3EuclideanNorm (x - x₀) ≤ 38 / 64} ×ˢ Set.Icc (a + 1 / 64) t₀,
|ω z| ≤ C) ∧ ω =ᵐ[MeasureTheory.volume.restrict
(CKN.Foundation.Parabolic.vec3Ball x₀ (38 / 64) ×ˢ Set.Ioo (a + 1 / 64) t₀)]
w
A continuous bounded representative on the closed box, from heat equations for the field and its first and second spatial weak derivatives.