The weak gradient of a weak heat solution

The mollified gradients (∂ⱼρₙ) ⋆ w form a Cauchy sequence in L² of the slab. Their limit is the weak spatial gradient of w (lem:localized-vorticity-energy).

noncomputable def ESS.vlGrad (w : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (n : ℕ) (j : Fin 3) : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ

The mollified gradient component.

Equations

• ESS.vlGrad w n j p = CKN.vlConvT (CKN.vlDeriv (CKN.vlMoll n) j) w p.1 p.2

theorem ESS.vlGrad_memLp {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) : MeasureTheory.MemLp (vlGrad w n j) 2 (MeasureTheory.volume.restrict (CKN.vlSlab a τ))

theorem ESS.vlGrad_sub_sq_le {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 m : ℕ) (j : Fin 3) : ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a τ, (vlGrad w n j p - vlGrad w m j p) ^ 2 ≤ 2 * vlErr w₀ w H f a τ n + 2 * vlErr w₀ w H f a τ m

The gradient Cauchy estimate.

noncomputable def ESS.vlGradLimit {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) : ↥(MeasureTheory.Lp ℝ 2 (MeasureTheory.volume.restrict (CKN.vlSlab a τ)))

The limit of the mollified gradients.

Equations

• ESS.vlGradLimit sol j = Filter.atTop.limUnder fun (n : ℕ) => MeasureTheory.MemLp.toLp (ESS.vlGrad w n j) ⋯

theorem ESS.vlGradLimit_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₀) (j : Fin 3) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.MemLp.toLp (vlGrad w n j) ⋯) Filter.atTop (nhds (vlGradLimit sol j))