The divergence-free condition on time slices

This file formalizes the Fubini reduction behind lem:divfree-slice and eq:divfree-ae of paper/ckn.tex. Clause (S2) of def:sws pairs the solution against the space-time test functions ∫ Σᵢ uᵢ ∂ᵢψ. Testing with a product ψ₀(x)θ(t) of a spatial test function ψ₀ ∈ C_c^∞(Ω) and a time cutoff θ ∈ C_c^∞(I), then applying Fubini, separates the time variable and shows that

∫_Ω Σᵢ uᵢ(x,s) ∂ᵢψ₀(x) dx = 0

for almost every s ∈ I. The null set a priori depends on ψ₀; obtaining one common null set requires a countable C¹-dense family of test functions and is not formalized here.

The product test function

The slice integral

Local integrability of the slice functional

The main statements

def CKN.SliceDivergenceFree (Ω : Set Foundation.Parabolic.Vec3) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (s : ℝ) : Prop

The weak divergence-free condition for the spatial slice at time s: the slice u(·,s) is divergence-free against every compactly supported smooth spatial test function contained in Ω, as in eq:divfree-common of paper/ckn.tex.

Equations

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

theorem CKN.divfree_slice_weak {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hS2 : ∀ ψ ∈ spaceTimeTestFunction Ω I, MeasureTheory.IntegrableOn (fun (z : Foundation.Parabolic.ParabolicPoint) => ∑ i : Fin 3, u z i * spatialPartial ψ i z) (tsupport ψ) MeasureTheory.volume ∧ ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω I, ∑ i : Fin 3, u z i * spatialPartial ψ i z = 0) (hI : IsOpen I) (ψ : Foundation.Parabolic.Vec3 → ℝ) : ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ Ω → ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∫ (x : Foundation.Parabolic.Vec3) in Ω, ∑ i : Fin 3, u (x, s) i * (fderiv ℝ ψ x) (basisVec i) = 0

The Fubini reduction of lem:divfree-slice and eq:divfree-ae: if the space-time test pairing (S2) of def:sws vanishes, then for each spatial test function ψ₀ the slice pairing vanishes for almost every time in I. The null set may depend on ψ₀.

theorem CKN.divfree_slice_weak_of_suitable {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (h : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) (ψ : Foundation.Parabolic.Vec3 → ℝ) : ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ Ω → ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∫ (x : Foundation.Parabolic.Vec3) in Ω, ∑ i : Fin 3, u (x, s) i * (fderiv ℝ ψ x) (basisVec i) = 0

The divergence-free slice conclusion read off from the suitable weak solution class of def:sws: for each spatial test function ψ₀ the slice pairing vanishes for almost every time in I.