The divergence of a test vector field

For an open set Ω of a finite-dimensional real normed space E, a test vector field φ ∈ 𝓓(Ω, E) has divergence div φ = tr (Dφ), which is again a test function on Ω. This file packages the divergence as a continuous linear map 𝓓(Ω, E) →L[ℝ] 𝓓(Ω, ℝ), in the style of Mathlib's TestFunction.fderivCLM, and expands it in the coordinates of any finite basis.

The divergence of test vector fields is the operator dual to the distributional gradient: the total variation of a function and the perimeter of a set are suprema of the pairings ∫ u div φ over test vector fields φ with ‖φ‖ ≤ 1.

Main declarations

• TestFunction.divergenceCLM: the divergence 𝓓(Ω, E) →L[ℝ] 𝓓(Ω, ℝ).
• TestFunction.divergenceCLM_apply: pointwise, it is the trace of the Fréchet derivative.
• TestFunction.divergenceCLM_monoCLM: the divergence commutes with extending a test vector field from Ω' to a larger open set Ω.
• TestFunction.divergenceCLM_postcompCLM_toSpanSingleton: the divergence of the vector field φ v is the directional derivative ∂_v φ.
• TestFunction.divergenceCLM_apply_eq_deriv: on the real line, the divergence of a test function is its derivative.
• TestFunction.divergenceCLM_apply_eq_sum: in a basis b, it is the sum of the derivatives of the coordinate functions b.repr (φ ·) i in the directions b i.
• TauCeti.divergenceCLM_translateTestFunction: the divergence of a translated test vector field is the translate of its divergence.
• TauCeti.integral_divergenceCLM_mul_congr_ae: the pairing ∫ u div φ only depends on u almost everywhere on Ω.
• TauCeti.trace_fderiv_smul and TauCeti.trace_fderiv_smul_const: the Leibniz rule div (χ φ) = χ div φ + Dχ φ for the divergence tr (D ·) of a vector field multiplied by a scalar function.
• TauCeti.exists_testFunction_sum_smul_comp_add: weighting translates of a test vector field φ by nonnegative smooth functions ζ k compactly supported in Ω with sum at most one gives a test vector field ∑ k, ζ k φ(· + τ k) on Ω, of norm at most one when ‖φ‖ ≤ 1, whose divergence is given by the Leibniz rule.

noncomputable def TestFunction.divergenceCLM {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {Ω : TopologicalSpace.Opens E} : TestFunction Ω E ⊤ →L[ℝ] TestFunction Ω ℝ ⊤

The divergence div φ = tr (Dφ) of a test vector field φ ∈ 𝓓(Ω, E), as a continuous linear map into the scalar test functions 𝓓(Ω, ℝ). It is the composite of the Fréchet derivative TestFunction.fderivCLM with the trace TauCeti.traceCLM.

@[simp]

theorem TestFunction.divergenceCLM_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {Ω : TopologicalSpace.Opens E} (φ : TestFunction Ω E ⊤) (x : E) : (divergenceCLM φ) x = (LinearMap.trace ℝ E) ↑(fderiv ℝ (⇑φ) x)

The divergence of a test vector field is pointwise the trace of its Fréchet derivative.

@[simp]

theorem TestFunction.divergenceCLM_monoCLM {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {Ω Ω' : TopologicalSpace.Opens E} (h : Ω' ≤ Ω) (φ : TestFunction Ω' E ⊤) : ⇑(divergenceCLM ((monoCLM ℝ) φ)) = ⇑(divergenceCLM φ)

The divergence of a test vector field extended from Ω' to a larger open set Ω is the divergence of the original field.

@[simp]

theorem TestFunction.divergenceCLM_postcompCLM_toSpanSingleton {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {Ω : TopologicalSpace.Opens E} (φ : TestFunction Ω ℝ ⊤) (v : E) : divergenceCLM ((postcompCLM (ContinuousLinearMap.toSpanSingleton ℝ v)) φ) = LineDeriv.lineDerivOp v φ

The divergence of the test vector field φ v, for a scalar test function φ and a fixed vector v, is the directional derivative ∂_v φ.

theorem TestFunction.divergenceCLM_apply_eq_deriv {Ω : TopologicalSpace.Opens ℝ} (φ : TestFunction Ω ℝ ⊤) (x : ℝ) : (divergenceCLM φ) x = deriv (⇑φ) x

On the real line, a test function is a test vector field whose divergence is its derivative.

theorem TestFunction.divergenceCLM_apply_eq_sum {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {Ω : TopologicalSpace.Opens E} {ι : Type u_2} [Fintype ι] (b : Module.Basis ι ℝ E) (φ : TestFunction Ω E ⊤) (x : E) : (divergenceCLM φ) x = ∑ i : ι, lineDeriv ℝ (fun (y : E) => (b.repr (φ y)) i) x (b i)

The divergence in a basis: div φ = ∑ i, ∂_{b i} (b.repr (φ ·) i).

@[simp]

theorem TauCeti.divergenceCLM_translateTestFunction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {Ω V : TopologicalSpace.Opens E} {h : E} (hVO : Set.MapsTo (fun (x : E) => x + h) ↑V ↑Ω) (φ : TestFunction V E ⊤) : TestFunction.divergenceCLM (translateTestFunction hVO φ) = translateTestFunction hVO (TestFunction.divergenceCLM φ)

The divergence of a translated test vector field is the translate of its divergence.

theorem TauCeti.trace_fderiv_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {χ : E → ℝ} {φ : E → E} {x : E} (hχ : DifferentiableAt ℝ χ x) (hφ : DifferentiableAt ℝ φ x) : (LinearMap.trace ℝ E) ↑(fderiv ℝ (fun (y : E) => χ y • φ y) x) = χ x * (LinearMap.trace ℝ E) ↑(fderiv ℝ φ x) + (fderiv ℝ χ x) (φ x)

Leibniz rule for the divergence: div (χ φ) = χ div φ + Dχ φ, where the divergence of a vector field is the trace of its Fréchet derivative.

theorem TauCeti.trace_fderiv_smul_const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {χ : E → ℝ} {x : E} (hχ : DifferentiableAt ℝ χ x) (v : E) : (LinearMap.trace ℝ E) ↑(fderiv ℝ (fun (y : E) => χ y • v) x) = (fderiv ℝ χ x) v

Divergence of a scalar function times a constant vector: div (χ v) = Dχ v.

theorem TauCeti.exists_testFunction_sum_smul_comp_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {Ω : TopologicalSpace.Opens E} {ι : Type u_2} {s : Finset ι} {ζ : ι → E → ℝ} (hζ : ∀ k ∈ s, ContDiff ℝ (↑⊤) (ζ k) ∧ HasCompactSupport (ζ k) ∧ tsupport (ζ k) ⊆ ↑Ω) (hζ0 : ∀ k ∈ s, ∀ (x : E), 0 ≤ ζ k x) (hζ1 : ∀ (x : E), ∑ k ∈ s, ζ k x ≤ 1) (φ : TestFunction Ω E ⊤) (hφ : ∀ (x : E), ‖φ x‖ ≤ 1) (τ : ι → E) : ∃ (Φ : TestFunction Ω E ⊤), (∀ (y : E), Φ y = ∑ k ∈ s, ζ k y • φ (y + τ k)) ∧ (∀ (y : E), ‖Φ y‖ ≤ 1) ∧ ∀ (y : E), (TestFunction.divergenceCLM Φ) y = ∑ k ∈ s, (ζ k y * (TestFunction.divergenceCLM φ) (y + τ k) + (fderiv ℝ (ζ k) y) (φ (y + τ k)))

Let ζ k, for k ∈ s, be nonnegative smooth functions compactly supported in Ω whose sum is at most one, and φ a test vector field on Ω with ‖φ‖ ≤ 1. For any vectors τ k, the field ∑ k ∈ s, ζ k φ(· + τ k) is a test vector field on Ω of norm at most one, whose divergence is given by the Leibniz rule div (ζ φ) = ζ div φ + Dζ φ. The translates φ(· + τ k) need not be supported in Ω: the weights ζ k cut them off.

theorem TauCeti.integral_divergenceCLM_mul_congr_ae {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {Ω : TopologicalSpace.Opens E} [MeasurableSpace E] {μ : MeasureTheory.Measure E} {u v : E → ℝ} (huv : u =ᵐ[μ.restrict ↑Ω] v) (φ : TestFunction Ω E ⊤) : ∫ (x : E), (TestFunction.divergenceCLM φ) x * u x ∂μ = ∫ (x : E), (TestFunction.divergenceCLM φ) x * v x ∂μ

The pairing ∫ u div φ of u with a test vector field φ on Ω only depends on u almost everywhere on Ω, since div φ vanishes off Ω.