Uniform-in-time bounds for backward mollifications of heat solutions #
For a square-integrable weak solution of the heat equation with square-integrable divergence-form
source on a box, the backward mollifications satisfy, for all small radii, a bound of their
spatial L² norm at every time up to the top, and are uniformly Cauchy in this norm (the
energy part of lem:localized-vorticity-energy and lem:local-heat-gain).
theorem
ESS.vorticity_heatSup_bm
{r R κ : ℝ}
(hr : 0 < r)
(hrR : r < R)
(hκ : 0 < κ)
:
∃ (C : ℝ),
0 ≤ C ∧ ∀ (x₀ : CKN.Foundation.Parabolic.Vec3) (a t₀ : ℝ) (w : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ)
(F : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
a + κ < t₀ →
t₀ ≤ a + 1 →
MeasureTheory.MemLp w 2
(MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ R ×ˢ Set.Ioo a t₀)) →
(∀ (j : Fin 3),
MeasureTheory.MemLp (F j) 2
(MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ R ×ˢ Set.Ioo a t₀))) →
(∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆ CKN.Foundation.Parabolic.vec3Ball x₀ R ×ˢ Set.Ioo a t₀ →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ R ×ˢ 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₀ R ×ˢ Set.Ioo a t₀, ∑ j : Fin 3, F j y * CKN.spatialPartial ψ j y) →
∀ (ε : ℕ → ℝ) (hεpos : ∀ (n : ℕ), 0 < ε n),
Filter.Tendsto ε Filter.atTop (nhds 0) →
(∀ᶠ (n : ℕ) in Filter.atTop, ∀ t ∈ Set.Icc (a + κ) t₀,
∫ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball x₀ r, CKN.vorticityBackMollify (CKN.Foundation.Parabolic.vec3Ball x₀ R ×ˢ Set.Ioo a t₀) w (ε n)
⋯ (x, t) ^ 2 ≤ (C * ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ R ×ˢ Set.Ioo a t₀, w y ^ 2 + ∑ j : Fin 3, F j y ^ 2) + 1) ∧ ∀ (δ : ℝ),
0 < δ →
∀ᶠ (p : ℕ × ℕ) in Filter.atTop, ∀ t ∈ Set.Icc (a + κ) t₀,
∫ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball x₀ r, (CKN.vorticityBackMollify (CKN.Foundation.Parabolic.vec3Ball x₀ R ×ˢ Set.Ioo a t₀) w
(ε p.1) ⋯ (x, t) - CKN.vorticityBackMollify (CKN.Foundation.Parabolic.vec3Ball x₀ R ×ˢ Set.Ioo a t₀)
w (ε p.2) ⋯ (x, t)) ^ 2 ≤ δ
Uniform-in-time bounds and the uniform Cauchy property for backward mollifications of a weak heat solution.