The slice energy balance of a linear Stokes-type system #

Let v solve ∂ₜv - Δv + div H + ∇q = 0 weakly on ℝ³ × (c, d), tested against smooth compactly supported vector fields, with div v = 0 and all fields square integrable. At almost every time the equation holds against every spatial test field; approximating the slice v(t) ∈ H¹ by smooth compactly supported fields shows that it may be tested with v(t) itself, and the pressure drops out because div v(t) = 0. This gives ∫ v · ∂ₜv = -∫ |∇v|² + ∫ H : ∇v at almost every time (prop:lps-smoothing).

source

def ESS.lpsSmoothCompactFields :

Submodule ℝ (CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3)

Smooth compactly supported vector fields on ℝ³, as a real vector space.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem ESS.lpsSmoothCompactFields_component (ψ : ↥lpsSmoothCompactFields) (i : Fin 3) :

(ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => ↑ψ x i) ∧ HasCompactSupport fun (x : CKN.Foundation.Parabolic.Vec3) => ↑ψ x i

source

noncomputable def ESS.lpsTestData :

↥lpsSmoothCompactFields →ₗ[ℝ ] Fin 3 ⊕ Fin 3 × Fin 3 → CKN.Foundation.Parabolic.Vec3 → ℝ

The test data of a vector field: its components and their first partials.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo c d), 2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, v (x, t) i * Dtv (x, t) i = (-2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, Dv (x, t) i j ^ 2) + 2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, H (x, t) i j * Dv (x, t) i j

At almost every time, a weak solution of ∂ₜv - Δv + div H + ∇q = 0 on ℝ³ × (c, d) with div v = 0 satisfies the slice energy balance ∫ v · ∂ₜv = -∫ |∇v|² + ∫ H : ∇v (prop:lps-smoothing).

Documentation

LeanPool.EscauriazaSereginSverak.LPS.SmoothingEnergyIdentitySlice

The slice energy balance of a linear Stokes-type system #