The local L¹ norm by duality with test vector fields

Let Ω be an open set of a finite-dimensional real normed space E, let F be a real Hilbert space, and let G : E → F →L[ℝ] ℝ be a field of continuous linear functionals that is locally integrable on Ω. Against an additive Haar measure μ,

∫⁻ x in Ω, ‖G x‖ₑ ∂μ = ⨆ { ∫ G x (φ x) ∂μ | φ ∈ 𝓓(Ω, F), ‖φ x‖ ≤ 1 for all x }

(MeasureTheory.LocallyIntegrableOn.iSup_ofReal_integral_apply_eq_setLIntegral_enorm), with both sides possibly infinite. The bound of each pairing by ∫_Ω ‖G‖ holds for every measure and every real normed space F (TestFunction.enorm_integral_apply_le_setLIntegral_enorm).

This duality identifies a supremum over test vector fields, such as the total variation of a function on Ω, with the integral of a pointwise norm. For a weakly differentiable function it shows that the total variation is the integral of the norm of the weak derivative.

For the reverse inequality, fix a compact K ⊆ Ω and let g x ∈ F be the Riesz representative of G x. The unit field x ↦ ‖g x‖⁻¹ • g x on K, extended by zero, is mollified by normalized bumps of shrinking support. The mollifications are test vector fields on Ω of norm at most one, they converge almost everywhere by the Lebesgue differentiation theorem, and dominated convergence turns their pairings with G into ∫_K ‖G‖. An exhaustion of Ω by compact sets concludes.

Main declarations

• TestFunction.enorm_integral_apply_le_setLIntegral_enorm: |∫ G φ| ≤ ∫_Ω ‖G‖ for a test vector field φ on Ω with ‖φ‖ ≤ 1.
• MeasureTheory.LocallyIntegrableOn.iSup_ofReal_integral_apply_eq_setLIntegral_enorm: the supremum of the pairings is ∫_Ω ‖G‖.

References

• L. C. Evans, R. F. Gariepy, Measure Theory and Fine Properties of Functions, revised edition, §5.1 (the variation of a Sobolev function).

theorem TestFunction.enorm_integral_apply_le_setLIntegral_enorm {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [NormedAddCommGroup F] [NormedSpace ℝ F] (φ : TestFunction Ω F ⊤) (hφ : ∀ (x : E), ‖φ x‖ ≤ 1) (G : E → F →L[ℝ] ℝ) : ‖∫ (x : E), (G x) (φ x) ∂μ‖ₑ ≤ ∫⁻ (x : E) in ↑Ω, ‖G x‖ₑ ∂μ

Pairing a field of continuous linear functionals G with a test vector field on Ω of norm at most one gives at most ∫_Ω ‖G‖.

theorem MeasureTheory.LocallyIntegrableOn.iSup_ofReal_integral_apply_eq_setLIntegral_enorm {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] {μ : Measure E} {Ω : TopologicalSpace.Opens E} [FiniteDimensional ℝ E] [BorelSpace E] [μ.IsAddHaarMeasure] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] {G : E → F →L[ℝ] ℝ} (hG : LocallyIntegrableOn G (↑Ω) μ) : ⨆ (φ : TestFunction Ω F ⊤), ⨆ (_ : ∀ (x : E), ‖φ x‖ ≤ 1), ENNReal.ofReal (∫ (x : E), (G x) (φ x) ∂μ) = ∫⁻ (x : E) in ↑Ω, ‖G x‖ₑ ∂μ

The local L¹ norm by duality. For a field G of continuous linear functionals on a real Hilbert space F that is locally integrable on Ω, against an additive Haar measure, ∫_Ω ‖G‖ is the supremum of ∫ G x (φ x) over test vector fields φ ∈ 𝓓(Ω, F) with ‖φ x‖ ≤ 1. Both sides may be infinite.