The pressure equation on almost every time slice

prop:lps-smoothing: let u be a strong solution with square-integrable space-time weak derivatives ∇u, ∇²u, ∂ₜu and pressure p. Testing the equation against separated fields χ(t) ψ(x) shows that for almost every time, and for every smooth compactly supported spatial field ψ, ∫ (∂ₜu - Δu + (u·∇)u)(t) · ψ = ∫ p(t) div ψ. The nonlinear term is moved onto (u·∇)u slice by slice, where u(t) ∈ H² is solenoidal. Hence at almost every time the pressure slice p(t) has the square-integrable weak gradient -(∂ₜu - Δu + (u·∇)u)(t).

def ESS.lpsScalarTests : Submodule ℝ (CKN.Foundation.Parabolic.Vec3 → ℝ)

Smooth compactly supported scalar functions on ℝ³, as a real vector space (prop:lps-smoothing).

Equations

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

noncomputable def ESS.lpsScalarTestData : ↥lpsScalarTests →ₗ[ℝ] Option (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ

The data of a scalar test in slice identities: the test itself (index none) and its first partial derivatives (index some k) (prop:lps-smoothing).

Equations

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

theorem ESS.lpsScalarTestData_memLp (φ : ↥lpsScalarTests) (o : Option (Fin 3)) : MeasureTheory.MemLp (lpsScalarTestData φ o) 2 MeasureTheory.volume

The data of a scalar test are square integrable (prop:lps-smoothing).

theorem ESS.lps_ae_forall_test_of_forall_ae {ν : MeasureTheory.Measure ℝ} {κ : Type u_1} [Fintype κ] {T : Type u_2} [AddCommGroup T] [Module ℝ T] (A : ℝ → κ → CKN.Foundation.Parabolic.Vec3 → ℝ) (hA : ∀ᵐ (t : ℝ) ∂ν, ∀ (k : κ), MeasureTheory.MemLp (A t k) 2 MeasureTheory.volume) (ι : T →ₗ[ℝ] κ → CKN.Foundation.Parabolic.Vec3 → ℝ) (hι : ∀ (ψ : T) (k : κ), MeasureTheory.MemLp (ι ψ k) 2 MeasureTheory.volume) (h : ∀ (ψ : T), ∀ᵐ (t : ℝ) ∂ν, ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : κ, A t k x * ι ψ k x = 0) : ∀ᵐ (t : ℝ) ∂ν, ∀ (ψ : T), ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : κ, A t k x * ι ψ k x = 0

Slice identities for a linear family of tests: if each identity holds for almost every time and the slice data are square integrable for almost every time, then almost every time satisfies all the identities simultaneously (prop:lps-smoothing).

theorem ESS.lps_strong_slice_pressure_equation {t₀ T : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {D2u : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {Dtu : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hsol : IsLpsStrongSolution t₀ T u Du p) (hderiv : CKN.HasSpaceTimeWeakDerivs Set.univ (Set.Ioo t₀ T) u Du D2u Dtu) (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)))) (hDu : MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)))) (hD2u : MeasureTheory.MemLp D2u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)))) (hDtu : MeasureTheory.MemLp Dtu 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)))) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo t₀ T), ∃ (Gq : Fin 3 → CKN.Foundation.Parabolic.Vec3 → ℝ), (∀ (i : Fin 3), MeasureTheory.MemLp (Gq i) 2 MeasureTheory.volume) ∧ MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => p (x, t)) 2 MeasureTheory.volume ∧ (∀ (i : Fin 3), CKN.HasWeakPartialDerivOn Set.univ i (fun (x : CKN.Vec 3) => p (x, t)) (Gq i)) ∧ ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), ∀ (i : Fin 3), Dtu (x, t) i - ∑ j : Fin 3, D2u (x, t) i j j + ∑ j : Fin 3, u (x, t) j * Du (x, t) i j + Gq i x = 0

prop:lps-smoothing: the pressure equation on almost every time slice. For almost every time t, the pressure slice p(t) is square integrable and has the square-integrable weak gradient Gq = -(∂ₜu - Δu + (u·∇)u)(t), where Δu = Σⱼ ∂ⱼ∂ⱼu and ((u·∇)u)ᵢ = Σⱼ uⱼ ∂ⱼuᵢ.