The vorticity representative and time-slice Sobolev export #
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_export
(Kw K1 K2 : ℝ)
:
∃ (C : ℝ) (Cslice : ℝ),
0 ≤ C ∧ 0 ≤ Cslice ∧ ∀ (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) →
∃ (ε : ℕ → ℝ) (hεpos : ∀ (n : ℕ), 0 < ε n) (ω :
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 ∧ TendstoUniformlyOn
(fun (n : ℕ) (z : CKN.Foundation.Parabolic.Vec3 × ℝ) =>
CKN.vorticityBackMollify
(CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo a t₀)
w (ε n) ⋯ z)
ω Filter.atTop
({x : CKN.Foundation.Parabolic.Vec3 | CKN.Foundation.Parabolic.vec3EuclideanNorm (x - x₀) ≤ 38 / 64} ×ˢ Set.Icc (a + 1 / 64) t₀) ∧ ∀ t ∈ Set.Icc (a + 1 / 64) t₀,
∃ (G : Fin 3 → CKN.Foundation.Parabolic.Vec3 → ℝ) (H :
Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 → ℝ),
(∀ (j : Fin 3),
CKN.HasWeakPartialDerivOn
(CKN.Foundation.Parabolic.vec3Ball x₀ (38 / 64)) j
(fun (x : CKN.Vec 3) => ω (x, t)) (G j)) ∧ (∀ (j k : Fin 3),
CKN.HasWeakPartialDerivOn
(CKN.Foundation.Parabolic.vec3Ball x₀ (38 / 64)) k (G j)
(H j k)) ∧ ∫ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball x₀ (38 / 64), ω (x, t) ^ 2 + ∑ j : Fin 3, G j x ^ 2 + ∑ j : Fin 3, ∑ k : Fin 3, H j k x ^ 2 ≤ Cslice * (|Kw| + |K1| + |K2| + 1)
A continuous representative and uniform time-slice H² data from heat equations for the field
and its first and second spatial weak derivatives.