The weak divergence of a weakly differentiable vector field

Let g : E → E be a vector field on an open set Ω of a finite-dimensional real inner product space, with weak derivative G : E → E →L[ℝ] E. Its divergence is the trace of its derivative, and this holds in the weak sense: for every test function φ on Ω,

∫ ⟪∇φ, g⟫ = -∫ φ • tr G.

Applied to the weak gradient g of a scalar function u, together with TauCeti.HasWeakFDerivOn.integral_laplacian_smul_eq_neg_integral_inner, this gives the pairing ∫ Δφ • u = ∫ φ • tr G. For an additive Haar measure, it says that the distributional Laplacian of a twice weakly differentiable function is the trace of its weak Hessian. This identity is what makes the weak formulation ∫ Δφ • u = ∫ φ • f of Poisson's equation Δu = f agree with the strong one, tr G = f almost everywhere, for twice weakly differentiable u.

Dually, a weakly differentiable function u : E → F with weak derivative U pairs with the divergence of a test vector field φ as ∫ div φ • u = -∫ U φ. This identity only needs a finite-dimensional real normed domain and a real normed codomain. For scalar u, it is the identity behind total variation, a supremum of the left-hand side over ‖φ‖ ≤ 1. Against an additive Haar measure, taking u = 1 gives ∫ div φ = 0.

No boundedness or boundary regularity of Ω is used. Except for ∫ div φ = 0, which needs an additive Haar measure, the measure need not be a Haar measure: the trace identity, the Laplacian identity and the pairing ∫ div φ • u = -∫ U φ all come from the defining integration-by-parts identities of weak derivatives. For a general measure these are adjoint identities relative to μ; their usual distributional interpretation requires an additive Haar measure.

Main declarations

• TauCeti.HasWeakFDerivOn.integral_inner_gradient_eq_neg_integral_smul_trace: the weak divergence of a weakly differentiable vector field is the trace of its weak derivative.
• TauCeti.HasWeakFDerivOn.integral_laplacian_smul_eq_integral_smul_trace: the Laplacian pairing of a twice weakly differentiable function is given by the trace of its weak Hessian.
• TauCeti.HasWeakFDerivOn.integral_divergenceCLM_smul_eq_neg_integral: a weakly differentiable function pairs with the divergence of a test vector field through its weak derivative.
• TestFunction.integral_divergenceCLM_eq_zero: the divergence of a test vector field has integral zero against an additive Haar measure.
• TauCeti.dist_integral_trace_fderiv_mul_le: the pairing ∫ div φ * u of C¹ vector fields supported in a fixed set K with a function integrable on K depends continuously on Dφ in the uniform norm.

References

• L. C. Evans, Partial Differential Equations, 2nd ed., §5.2.1 and §6.3.

theorem TauCeti.HasWeakFDerivOn.integral_inner_gradient_eq_neg_integral_smul_trace {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [OpensMeasurableSpace E] {g : E → E} {G : E → E →L[ℝ] E} (h : HasWeakFDerivOn μ Ω g G) (φ : TestFunction Ω ℝ ⊤) : ∫ (x : E), inner ℝ (gradient (⇑φ) x) (g x) ∂μ = -∫ (x : E), φ x • (LinearMap.trace ℝ E) ↑(G x) ∂μ

The weak divergence is the trace of the weak derivative. If the vector field g has weak derivative G on Ω, then for every test function φ on Ω, ∫ ⟪∇φ, g⟫ ∂μ = -∫ φ • tr G ∂μ.

theorem TauCeti.HasWeakFDerivOn.integral_laplacian_smul_eq_integral_smul_trace {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [OpensMeasurableSpace E] {u : E → ℝ} {g : E → E} {G : E → E →L[ℝ] E} (hu : HasWeakFDerivOn μ Ω u fun (x : E) => (innerSL ℝ) (g x)) (hg : HasWeakFDerivOn μ Ω g G) (φ : TestFunction Ω ℝ ⊤) : ∫ (x : E), Laplacian.laplacian (⇑φ) x • u x ∂μ = ∫ (x : E), φ x • (LinearMap.trace ℝ E) ↑(G x) ∂μ

The Laplacian pairing is given by the trace of the weak Hessian. If u has weak gradient g on Ω and g has weak derivative G there, then for every test function φ on Ω, ∫ Δφ • u ∂μ = ∫ φ • tr G ∂μ. For an additive Haar measure, this identifies the distributional Laplacian of u with the trace of its weak Hessian.

theorem TauCeti.HasWeakFDerivOn.integral_divergenceCLM_smul_eq_neg_integral {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [NormedSpace ℝ E] [FiniteDimensional ℝ E] [OpensMeasurableSpace E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {u : E → F} {U : E → E →L[ℝ] F} (h : HasWeakFDerivOn μ Ω u U) (φ : TestFunction Ω E ⊤) : ∫ (x : E), (TestFunction.divergenceCLM φ) x • u x ∂μ = -∫ (x : E), (U x) (φ x) ∂μ

Integration by parts against a divergence. If u : E → F has weak derivative U on Ω, then for every test vector field φ on Ω, ∫ div φ • u ∂μ = -∫ U φ ∂μ.

theorem TestFunction.integral_divergenceCLM_eq_zero {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [NormedSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] [μ.IsAddHaarMeasure] (φ : TestFunction Ω E ⊤) : ∫ (x : E), (divergenceCLM φ) x ∂μ = 0

The divergence of a test vector field has integral zero against an additive Haar measure: ∫ div φ ∂μ = 0.

theorem TauCeti.dist_integral_trace_fderiv_mul_le {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} [NormedSpace ℝ E] [FiniteDimensional ℝ E] [OpensMeasurableSpace E] {u : E → ℝ} {K : Set E} (hu : MeasureTheory.IntegrableOn u K μ) {f g : E → E} (hf : ContDiff ℝ 1 f) (hg : ContDiff ℝ 1 g) (hfK : tsupport f ⊆ K) (hgK : tsupport g ⊆ K) {ε : ℝ} (hε : ∀ (x : E), dist (fderiv ℝ f x) (fderiv ℝ g x) ≤ ε) : dist (∫ (x : E), (LinearMap.trace ℝ E) ↑(fderiv ℝ f x) * u x ∂μ) (∫ (x : E), (LinearMap.trace ℝ E) ↑(fderiv ℝ g x) * u x ∂μ) ≤ ‖traceCLM ℝ E‖ * ε * ∫ (x : E) in K, ‖u x‖ ∂μ

Vector fields supported in a fixed set K whose derivatives are uniformly close have close divergence pairings ∫ div φ * u dμ with a function u integrable on K. The constant is the norm of the trace times ∫_K |u| dμ. (If the two pairings are not integrable, both are 0.)