The energy estimate for a weak heat solution with L² data #
A distributional solution w ∈ L²(ℝ³ × (a, τ)) of ∂ₜ w - Δw = div H + f,
with H, f ∈ L² and initial trace w₀ ∈ L², has a continuous L²
representative Z on [a, τ] with Z(a) = w₀ and a weak spatial gradient
D ∈ L², and for every t ∈ [a, τ]
‖Z(t)‖² + ∫ₐᵗ ‖D‖² ≤ ‖w₀‖² + ∫ₐᵗ (‖H‖² + ‖w‖² + ‖f‖²)
(lem:localized-vorticity-energy).
theorem
ESS.vlConv_integral_mul_fderiv
{k h g : CKN.Foundation.Parabolic.Vec3 → ℝ}
(hk : CKN.IsVlKernel k)
(hh : MeasureTheory.MemLp h 2 MeasureTheory.volume)
(hg : ContDiff ℝ 1 g)
(hgc : HasCompactSupport g)
(j : Fin 3)
:
∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.vlConv k h x * (fderiv ℝ g x) (CKN.basisVec j) = -∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.vlConv (CKN.vlDeriv k j) h x * g x
Integration by parts of a kernel convolution against a compactly
supported C¹ spatial function.
theorem
ESS.vlGrad_weak_n
{a τ : ℝ}
{w f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
{H : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
{w₀ : CKN.Foundation.Parabolic.Vec3 → ℝ}
(sol : CKN.VlHeatSolution a τ w H f w₀)
(n : ℕ)
(j : Fin 3)
{φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hφ : φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a τ))
:
∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a τ, CKN.vlConvT (CKN.vlMoll n) w p.1 p.2 * CKN.spatialPartial φ j p = -∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a τ, vlGrad w n j p * φ p
Each mollified slice satisfies the weak-gradient identity.
noncomputable def
ESS.vlMollSlab
{a τ : ℝ}
{w f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
{H : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
{w₀ : CKN.Foundation.Parabolic.Vec3 → ℝ}
(sol : CKN.VlHeatSolution a τ w H f w₀)
(n : ℕ)
:
↥(MeasureTheory.Lp ℝ 2 (MeasureTheory.volume.restrict (CKN.vlSlab a τ)))
The mollified field as an element of L² of the slab.
Equations
- ESS.vlMollSlab sol n = MeasureTheory.MemLp.toLp (fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.vlConvT (CKN.vlMoll n) w p.1 p.2) ⋯
Instances For
theorem
ESS.vlMollSlab_tendsto
{a τ : ℝ}
{w f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
{H : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
{w₀ : CKN.Foundation.Parabolic.Vec3 → ℝ}
(sol : CKN.VlHeatSolution a τ w H f w₀)
:
Filter.Tendsto (fun (n : ℕ) => vlMollSlab sol n) Filter.atTop (nhds (MeasureTheory.MemLp.toLp w ⋯))
theorem
ESS.vlGradLimit_weak
{a τ : ℝ}
{w f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
{H : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
{w₀ : CKN.Foundation.Parabolic.Vec3 → ℝ}
(sol : CKN.VlHeatSolution a τ w H f w₀)
(j : Fin 3)
{φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hφ : φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a τ))
:
∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a τ, w p * CKN.spatialPartial φ j p = -∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a τ, ↑↑(vlGradLimit sol j) p * φ p
The limit gradient is the weak spatial gradient.