Pointwise bounds on a density from its pairings with test vector fields

Let Ω be an open set of a finite-dimensional real normed space E, let ρ be a measure on Ω and let h : Ω → F be locally integrable, with values in a separable real inner product space F. If every pairing of h with a test vector field φ ∈ 𝓓(Ω, F) of norm at most one supported in an open set U is bounded by the integral of a fixed weight k over U,

|∫ ⟪φ x, h x⟫ ∂ρ| ≤ ∫⁻ x in U, k x ∂ρ,

then ‖h x‖ ≤ k x for ρ-almost every x (TauCeti.ae_enorm_le_of_forall_enorm_integral_inner_le). For k = 0 this is the fundamental lemma of the calculus of variations on Ω. With k the density of a second measure ν with respect to ρ, it says that a functional bounded on test vector fields by ν is represented against ρ by a density pointwise dominated by that of ν. This is how a measure-valued derivative is shown to be absolutely continuous with respect to its variation, with a density of norm at most one.

The proof first tests against smooth cutoffs equal to one on a compact set K and supported in shrinking neighbourhoods of K, which gives |∫_K h| ≤ ∫⁻_K k. Inner regularity (TauCeti.enorm_setIntegral_le_of_forall_isClosed_subset) extends this to measurable subsets of a compact set, and the scalar case follows by comparing set integrals.

The vector case is proved more generally for a density h : Ω → StrongDual ℝ F with values in the normed dual of a separable real normed space, paired with test vector fields by evaluation, x ↦ h x (φ x), and bounded in the dual norm: it tests the scalar components x ↦ h x w for w in a countable dense subset of F. This is the form needed for currents, whose densities with respect to their mass measures take values in the dual of the space of forms with its comass norm. The inner product statement is its special case through innerSL.

The same scalar argument, with k the positive part of h, shows that a scalar density whose pairings with nonnegative test functions are nonnegative is itself nonnegative almost everywhere (TauCeti.ae_nonneg_of_forall_integral_mul_nonneg).

Main declarations

• TauCeti.ae_enorm_le_of_forall_enorm_integral_apply_le: the pointwise bound ‖h‖ ≤ k in the dual norm.
• TauCeti.ae_enorm_le_of_forall_enorm_integral_inner_le: the pointwise bound ‖h‖ ≤ k for an inner product space.
• TauCeti.ae_nonneg_of_forall_integral_mul_nonneg: nonnegativity from nonnegative pairings.

References

• L. C. Evans, R. F. Gariepy, Measure Theory and Fine Properties of Functions, revised edition, §1.8 (the representation of functionals bounded on compactly supported vector fields).

theorem TauCeti.ae_nonneg_of_forall_integral_mul_nonneg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {Ω : TopologicalSpace.Opens E} {ρ : MeasureTheory.Measure ↥Ω} {h : ↥Ω → ℝ} (hh : MeasureTheory.LocallyIntegrable h ρ) (H : ∀ (ψ : TestFunction Ω ℝ ⊤), (∀ (x : E), 0 ≤ ψ x) → 0 ≤ ∫ (x : ↥Ω), ψ ↑x * h x ∂ρ) : ∀ᵐ (x : ↥Ω) ∂ρ, 0 ≤ h x

A density with nonnegative pairings is nonnegative. If h : Ω → ℝ is locally integrable for a measure ρ on Ω and 0 ≤ ∫ ψ x * h x ∂ρ for every nonnegative test function ψ on Ω, then 0 ≤ h x for ρ-almost every x.

theorem TauCeti.ae_enorm_le_of_forall_enorm_integral_apply_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {Ω : TopologicalSpace.Opens E} {ρ : MeasureTheory.Measure ↥Ω} {k : ↥Ω → ENNReal} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace.SeparableSpace F] {h : ↥Ω → StrongDual ℝ F} (hh : MeasureTheory.LocallyIntegrable h ρ) (hkm : Measurable k) (hk : ∀ (K : Set ↥Ω), IsCompact K → ∫⁻ (x : ↥Ω) in K, k x ∂ρ ≠ ⊤) (H : ∀ U ≤ Ω, ∀ (φ : TestFunction Ω F ⊤), tsupport ⇑φ ⊆ ↑U → (∀ (x : E), ‖φ x‖ ≤ 1) → ‖∫ (x : ↥Ω), (h x) (φ ↑x) ∂ρ‖ₑ ≤ ∫⁻ (x : ↥Ω) in Subtype.val ⁻¹' ↑U, k x ∂ρ) : ∀ᵐ (x : ↥Ω) ∂ρ, ‖h x‖ₑ ≤ k x

A dual-valued density bounded on test vector fields is pointwise bounded. Let h : Ω → StrongDual ℝ F be locally integrable for a measure ρ on Ω, and let k be a measurable weight with finite integral over every compact subset of Ω. If for every open U ⊆ Ω and every test vector field φ supported in U with ‖φ x‖ ≤ 1 we have |∫ h x (φ x) ∂ρ| ≤ ∫⁻ x in U, k x ∂ρ, then the dual norm satisfies ‖h x‖ ≤ k x for ρ-almost every x.

theorem TauCeti.ae_enorm_le_of_forall_enorm_integral_inner_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {Ω : TopologicalSpace.Opens E} {ρ : MeasureTheory.Measure ↥Ω} {k : ↥Ω → ENNReal} {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace.SeparableSpace F] {h : ↥Ω → F} (hh : MeasureTheory.LocallyIntegrable h ρ) (hkm : Measurable k) (hk : ∀ (K : Set ↥Ω), IsCompact K → ∫⁻ (x : ↥Ω) in K, k x ∂ρ ≠ ⊤) (H : ∀ U ≤ Ω, ∀ (φ : TestFunction Ω F ⊤), tsupport ⇑φ ⊆ ↑U → (∀ (x : E), ‖φ x‖ ≤ 1) → ‖∫ (x : ↥Ω), inner ℝ (φ ↑x) (h x) ∂ρ‖ₑ ≤ ∫⁻ (x : ↥Ω) in Subtype.val ⁻¹' ↑U, k x ∂ρ) : ∀ᵐ (x : ↥Ω) ∂ρ, ‖h x‖ₑ ≤ k x

A density bounded on test vector fields is pointwise bounded. Let h : Ω → F be locally integrable for a measure ρ on Ω, with values in a separable real inner product space F, and let k be a measurable weight with finite integral over every compact subset of Ω. If for every open U ⊆ Ω and every test vector field φ supported in U with ‖φ x‖ ≤ 1 we have |∫ ⟪φ x, h x⟫ ∂ρ| ≤ ∫⁻ x in U, k x ∂ρ, then ‖h x‖ ≤ k x for ρ-almost every x.