Admissible Weak Divergence

Supporting results for the Constantin–Ignatova–Vicol axisymmetric regularity theorem.

theorem CIV.isAdmissibleDrift_weak_divergence {m : ℕ} {I : Set ℝ} {B : CKN.Vec m × ℝ → CKN.Vec m} {divB : CKN.Vec m × ℝ → ℝ} (hB : IsAdmissibleDrift m I B divB) {J : Set ℝ} (hJ : IsCompact J) (hJI : J ⊆ I) : ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict J, ∀ (ψ : CKN.Vec m → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∫ (x : CKN.Vec m), divB (x, τ) * ψ x = -∫ (x : CKN.Vec m), ∑ i : Fin m, B (x, τ) i * (fderiv ℝ ψ x) (CKN.basisVec i)

Extract the weak divergence identity from an IsAdmissibleDrift hypothesis. For almost every τ ∈ J the slice B(·, τ) has divB(·, τ) as its weak divergence: ∫ divB(·,τ) ψ = -∫ ∑ᵢ B(·,τ)ᵢ (∂ᵢψ).