The directional derivatives of a function of locally bounded variation are measures

Let Ω be an open set of a finite-dimensional real inner product space E and let u : E → ℝ. For locally integrable u, the pairing of the directional derivative ∂_v u with a test function φ is -∫ ∂_v φ * u, and ∂_v φ is the divergence of the test vector field φ v. Hence the variational total variation |Du|(Ω) bounds it: |∫ ∂_v φ * u| ≤ ‖v‖ ‖φ‖_∞ |Du|(Ω) (TestFunction.ofReal_abs_integral_lineDeriv_mul_le_enorm_mul_enorm_mul_totalVariationOn).

The distributional derivative is taken of Distribution.ofFun Ω u μ ⊤. When u is locally integrable on Ω this is integration against u, so ∂_v u (φ) = -∫ ∂_v φ * u; otherwise Distribution.ofFun is zero by convention, and so is its derivative.

If u has locally finite variation on Ω, meaning that every compact K ⊆ Ω has an open neighbourhood U with |Du|(U) < ∞, this makes each distributional derivative ∂_v u ∈ 𝓓'(Ω, ℝ) a distribution of order zero. It is therefore a signed Radon measure: there are regular measures ν₁ and ν₂ on Ω, finite on compact sets, with ∂_v u (φ) = ∫ φ dν₁ - ∫ φ dν₂ for every test function φ (TauCeti.exists_regular_lineDeriv_ofFun_apply_eq). No global finiteness of the variation is needed, so this covers functions of locally bounded variation on unbounded open sets.

Main results

• TestFunction.ofReal_abs_integral_lineDeriv_mul_le_enorm_mul_enorm_mul_totalVariationOn: the directional derivative pairing is bounded by ‖v‖ ‖φ‖_∞ |Du|(Ω).
• TauCeti.exists_regular_lineDeriv_ofFun_apply_eq: the directional derivatives of a function of locally finite variation on Ω are differences of regular measures on Ω.

References

• L. Ambrosio, N. Fusco, D. Pallara, Functions of Bounded Variation and Free Discontinuity Problems, §3.1.
• L. C. Evans, R. F. Gariepy, Measure Theory and Fine Properties of Functions, revised edition, §5.1 (the structure theorem for functions of locally bounded variation).

theorem TestFunction.ofReal_abs_integral_lineDeriv_mul_le_enorm_mul_enorm_mul_totalVariationOn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} {u : E → ℝ} (φ : TestFunction Ω ℝ ⊤) (v : E) : ENNReal.ofReal |∫ (x : E), (LineDeriv.lineDerivOp v φ) x * u x ∂μ| ≤ ‖v‖ₑ * ‖{ toFun := ⇑φ, continuous_toFun := ⋯, map_bounded' := ⋯ }‖ₑ * TauCeti.totalVariationOn μ Ω u

The directional derivative is bounded by the total variation. For a test function φ on Ω and a direction v, |∫ ∂_v φ * u| ≤ ‖v‖ ‖φ‖_∞ |Du|(Ω).

theorem TauCeti.exists_regular_lineDeriv_ofFun_apply_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} {u : E → ℝ} [BorelSpace E] (hu : ∀ (K : Set E), IsCompact K → K ⊆ ↑Ω → ∃ (U : TopologicalSpace.Opens E), K ⊆ ↑U ∧ totalVariationOn μ U u ≠ ⊤) (v : E) : ∃ (ν₁ : MeasureTheory.Measure ↥Ω) (ν₂ : MeasureTheory.Measure ↥Ω), ν₁.Regular ∧ ν₂.Regular ∧ ∀ (φ : TestFunction Ω ℝ ⊤), (LineDeriv.lineDerivOp v (Distribution.ofFun Ω u μ ⊤)) φ = ∫ (x : ↥Ω), φ ↑x ∂ν₁ - ∫ (x : ↥Ω), φ ↑x ∂ν₂

The directional derivatives of a function of locally finite variation are signed Radon measures. If every compact K ⊆ Ω has an open neighbourhood U on which u has finite total variation, then for every direction v there are regular measures ν₁ and ν₂ on Ω with ∂_v u (φ) = ∫ φ dν₁ - ∫ φ dν₂ for every test function φ, where ∂_v u is the derivative of the distribution Distribution.ofFun Ω u μ ⊤. If u is locally integrable on Ω, this is the distributional derivative of u, ∂_v u (φ) = -∫ ∂_v φ * u; otherwise Distribution.ofFun is zero by convention and the statement is trivial. The measures are finite on compact subsets of Ω but need not be finite.