Mollified pairings as primitives of their fluxes

For a smooth compactly supported kernel ρ, the mollified component y ↦ ∫ u(x,t)_k ρ(y - x) dx is, at every point y, the primitive in time of the momentum flux tested against ρ(y - ·). This is the pointwise-in-space calculus behind the cross-testing identity of lem:pv-serrin-uniqueness.

noncomputable def ESS.serrinMol (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (ρ : CKN.Foundation.Parabolic.Vec3 → ℝ) (k : Fin 3) (y : CKN.Foundation.Parabolic.Vec3) (t : ℝ) : ℝ

The mollified kth component of the time slice at time t, evaluated at y.

Equations

• ESS.serrinMol u ρ k y t = ∫ (x : CKN.Foundation.Parabolic.Vec3), u (x, t) k * ρ (y - x)

noncomputable def ESS.serrinMolFluxDensity (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 → ℝ) (k : Fin 3) (y : CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ℝ

The momentum flux density tested against the translated kernel ρ(y - ·) in the kth component.

Equations

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

noncomputable def ESS.serrinMolFlux (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 → ℝ) (k : Fin 3) (y : CKN.Foundation.Parabolic.Vec3) (τ : ℝ) : ℝ

The spatially integrated flux of the mollified kth component.

Equations

• ESS.serrinMolFlux u Du p ρ k y τ = ∫ (x : CKN.Foundation.Parabolic.Vec3), ESS.serrinMolFluxDensity u Du p ρ k y (x, τ)

def ESS.serrinKernelTest (ρ : CKN.Foundation.Parabolic.Vec3 → ℝ) (k : Fin 3) (y : CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3

The translated and reflected kernel placed in the kth component.

Equations

• ESS.serrinKernelTest ρ k y x i = if i = k then ρ (y - x) else 0

theorem ESS.spatialDeriv_reflect {ρ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hρ : ContDiff ℝ (↑⊤) ρ) (y : CKN.Foundation.Parabolic.Vec3) (j : Fin 3) (x : CKN.Foundation.Parabolic.Vec3) : CKN.spatialDeriv (fun (x' : CKN.Foundation.Parabolic.Vec3) => ρ (y - x')) j x = -CKN.spatialDeriv ρ j (y - x)

theorem ESS.serrinKernelTest_contDiff {ρ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hρ : ContDiff ℝ (↑⊤) ρ) (k : Fin 3) (y : CKN.Foundation.Parabolic.Vec3) : ContDiff ℝ (↑⊤) (serrinKernelTest ρ k y)

theorem ESS.serrinKernelTest_hasCompactSupport {ρ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hρc : HasCompactSupport ρ) (k : Fin 3) (y : CKN.Foundation.Parabolic.Vec3) : HasCompactSupport (serrinKernelTest ρ k y)

theorem ESS.serrinFlux_kernelTest {ρ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hρ : ContDiff ℝ (↑⊤) ρ) (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 → ℝ) (k : Fin 3) (y : CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : serrinFlux u Du p (serrinKernelTest ρ k y) z = serrinMolFluxDensity u Du p ρ k y z

theorem ESS.serrinPairing_kernelTest (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (ρ : CKN.Foundation.Parabolic.Vec3 → ℝ) (k : Fin 3) (y x : CKN.Foundation.Parabolic.Vec3) (t : ℝ) : ∑ i : Fin 3, u (x, t) i * serrinKernelTest ρ k y x i = u (x, t) k * ρ (y - x)

theorem ESS.serrinMol_slab {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 → ℝ} (hρ : ContDiff ℝ (↑⊤) ρ) (hρc : HasCompactSupport ρ) (k : Fin 3) (y : CKN.Foundation.Parabolic.Vec3) : MeasureTheory.IntegrableOn (serrinMolFlux u Du p ρ k y) (Set.Ioo 0 T) MeasureTheory.volume ∧ ∀ t ∈ Set.Icc 0 T, serrinMol u ρ k y t = serrinMol u ρ k y 0 + ∫ (τ : ℝ) in 0..t, serrinMolFlux u Du p ρ k y τ

The mollified component of a finite-energy weak solution is, at every point, the primitive of its tested flux.

theorem ESS.serrinMol_product {T : ℝ} {a b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {u v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {pu pv : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hU : IsSerrinWeakSolution T a u Du pu) (hV : IsSerrinWeakSolution T b v Dv pv) {ρ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hρ : ContDiff ℝ (↑⊤) ρ) (hρc : HasCompactSupport ρ) (k : Fin 3) (y : CKN.Foundation.Parabolic.Vec3) {t : ℝ} (ht : t ∈ Set.Icc 0 T) : serrinMol v ρ k y t * serrinMol u ρ k y t = serrinMol v ρ k y 0 * serrinMol u ρ k y 0 + ∫ (τ : ℝ) in 0..t, serrinMolFlux v Dv pv ρ k y τ * serrinMol u ρ k y τ + serrinMol v ρ k y τ * serrinMolFlux u Du pu ρ k y τ

The product of two mollified components is the primitive of the product rule expression.