Time-slab identities for a fixed spatial test

For a Leray–Hopf solution whose momentum identity holds with a pressure, the pairing of the specified time slices with a fixed smooth compactly supported spatial field evolves by the integrated flux. This is the pairing formula used for the cross-testing identity in lem:pv-serrin-uniqueness.

noncomputable def ESS.serrinFlux (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 → ℝ) (ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ℝ

The momentum flux density of (u, Du, p) against a fixed spatial field ψ: convection, diffusion and pressure terms.

Equations

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

def ESS.serrinPairing (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ℝ

The pairing density of a velocity with a fixed spatial field.

Equations

• ESS.serrinPairing u ψ z = ∑ i : Fin 3, u z i * ψ z.1 i

theorem ESS.serrin_spatialDeriv_eq_zero_of_not_mem_tsupport {f : CKN.Foundation.Parabolic.Vec3 → ℝ} {x : CKN.Foundation.Parabolic.Vec3} (hx : x ∉ tsupport f) (j : Fin 3) : CKN.spatialDeriv f j x = 0

A spatial derivative vanishes outside the topological support.

theorem ESS.serrinFlux_eq_zero_of_not_mem {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 → ℝ} {ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z.1 ∉ tsupport ψ) : serrinFlux u Du p ψ z = 0

Outside the support of the spatial field, the flux density vanishes.

theorem ESS.serrin_momentum_pressure_separated {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 → ℝ} (hmom : ∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo 0 T), ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 T), -∑ i : Fin 3, u z i * CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) z - ∑ i : Fin 3, ∑ j : Fin 3, u z i * u z j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3, ∑ j : Fin 3, Du z i j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z - p z * ∑ i : Fin 3, CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) i z - ∑ i : Fin 3, 0 z i * φ z i = 0) {ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hψsmooth : ContDiff ℝ (↑⊤) ψ) (hψcompact : HasCompactSupport ψ) {η : ℝ → ℝ} (hη : CKN.IsIntervalTest (Set.Ioo 0 T) η) : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 T), -(serrinPairing u ψ z * deriv η z.2) - serrinFlux u Du p ψ z * η z.2 = 0

The separated test ψ(x) η(t) in the momentum identity with pressure.

theorem ESS.serrinWeak_velocity_memLp_two {T : ℝ} {a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {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 → ℝ} (hU : IsSerrinWeakSolution T a u Du p) : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))

The velocity of a finite-energy weak solution is square integrable on the space-time slab.

theorem ESS.serrinWeak_gradient_memLp_two {T : ℝ} {a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {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 → ℝ} (hU : IsSerrinWeakSolution T a u Du p) : MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))

The weak gradient of a finite-energy weak solution is square integrable on the slab.

theorem ESS.serrinWeak_tensor_memLp_one {T : ℝ} {a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {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 → ℝ} (hU : IsSerrinWeakSolution T a u Du p) (i j : Fin 3) : MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => u z i * u z j) 1 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))

The velocity tensor of a finite-energy weak solution is integrable on the slab.

theorem ESS.serrin_integrable_restrict_of_memLp {T : ℝ} {K : Set CKN.Foundation.Parabolic.Vec3} (hK : IsCompact K) {f : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {q : ENNReal} (hq : 1 ≤ q) (hf : MeasureTheory.MemLp f q (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) : MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => f z) ((MeasureTheory.volume.restrict K).prod (MeasureTheory.volume.restrict (Set.Ioo 0 T)))

A slab field in L^q with q ≥ 1 is integrable on a compact spatial set times the time interval.

theorem ESS.serrin_slab_identity {T : ℝ} {a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {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 → ℝ} (hU : IsSerrinWeakSolution T a u Du p) {ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hψsmooth : ContDiff ℝ (↑⊤) ψ) (hψcompact : HasCompactSupport ψ) : MeasureTheory.IntegrableOn (fun (τ : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), serrinFlux u Du p ψ (x, τ)) (Set.Ioo 0 T) MeasureTheory.volume ∧ ∀ t ∈ Set.Icc 0 T, ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, u (x, t) i * ψ x i = (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, u (x, 0) i * ψ x i) + ∫ (τ : ℝ) in 0..t, ∫ (x : CKN.Foundation.Parabolic.Vec3), serrinFlux u Du p ψ (x, τ)

The pairing of the specified time slices of a finite-energy weak solution with a fixed smooth compactly supported spatial field is the initial pairing plus the time integral of the momentum flux, at every time of the closed interval.