Integrals of test functions against measures finite on compact sets

Let Ω be an open set of a real normed space E. A test function φ ∈ 𝓓^{n}(Ω, F) restricts to a compactly supported continuous function on the subspace Ω. For a test function φ ∈ 𝓓(Ω, F) supported in a compact K ⊆ Ω and a measure ν on the subspace Ω that is finite on compact sets, the integral of φ against ν is bounded by the sup norm: ‖∫ φ dν‖ ≤ ν(K) ‖φ‖_∞.

This is the estimate showing that integration against such a measure is a distribution of order zero. Through a continuous bilinear map, a test function also pairs integrably with every function that is locally integrable for a measure on Ω.

Every nonempty open subset of the domain also contains a nonnegative integral-one test, for any locally finite measure positive on nonempty open sets. The construction normalizes Mathlib's exists_contDiff_tsupport_subset by its positive integral. These tests recover the coefficient of a constant distribution, including on arbitrarily small overlap neighborhoods.

Against an additive Haar measure, the directional derivative of a test function has integral zero, by Mathlib's integration by parts against the constant function 1.

Main definitions

• TestFunction.toCompactlySupportedContinuousMap: the restriction of a test function on Ω to a compactly supported continuous function on the subspace Ω.

Main results

• TestFunction.exists_nonneg_integral_eq_one: a nonnegative integral-one test supported in any nonempty open subset of the domain.

• TestFunction.norm_integral_le_measureReal_mul_norm: ‖∫ φ dν‖ ≤ ν(K) ‖φ‖_∞ for a test function φ supported in a compact K ⊆ Ω.

• TestFunction.integrable_bilin_subtype: x ↦ B (φ x) (g x) is integrable for g locally integrable for a measure on Ω.

• TestFunction.neg_integral_smul_neg_add_eq: the integral of a test function against the right-hand side -(f + ∑ᵢⱼ Gᵢⱼ) of a weak derivative equation.

• TestFunction.integrable_inner_subtype: the pairing ⟪φ x, v x⟫ of a test vector field with a locally integrable field is integrable.

• TestFunction.enorm_integral_inner_le_withDensity: the pairing of a test field supported in U and bounded by 1 with v is at most the mass of |v| m on U.

• TestFunction.integral_lineDeriv_eq_zero: ∫ ∂_w φ dμ = 0 for an additive Haar measure μ.

def TestFunction.toCompactlySupportedContinuousMap {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} (φ : TestFunction Ω F n) : CompactlySupportedContinuousMap (↥Ω) F

The restriction of a test function on Ω to a compactly supported continuous function on the subspace Ω.

@[simp]

theorem TestFunction.toCompactlySupportedContinuousMap_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} (φ : TestFunction Ω F n) (x : ↥Ω) : φ.toCompactlySupportedContinuousMap x = φ ↑x

@[simp]

theorem TestFunction.toCompactlySupportedContinuousMap_zero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} : toCompactlySupportedContinuousMap 0 = 0

@[simp]

theorem TestFunction.toCompactlySupportedContinuousMap_add {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} (φ ψ : TestFunction Ω F n) : (φ + ψ).toCompactlySupportedContinuousMap = φ.toCompactlySupportedContinuousMap + ψ.toCompactlySupportedContinuousMap

@[simp]

theorem TestFunction.toCompactlySupportedContinuousMap_smul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {R : Type u_3} [Semiring R] [Module R F] [SMulCommClass ℝ R F] [ContinuousConstSMul R F] (c : R) (φ : TestFunction Ω F n) : (c • φ).toCompactlySupportedContinuousMap = c • φ.toCompactlySupportedContinuousMap

theorem TestFunction.norm_integral_le_measureReal_mul_norm {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} [MeasurableSpace E] (φ : TestFunction Ω F ⊤) {K : Set E} (hK : IsCompact K) (hKΩ : K ⊆ ↑Ω) (hφ : tsupport ⇑φ ⊆ K) (ν : MeasureTheory.Measure ↥Ω) [MeasureTheory.IsFiniteMeasureOnCompacts ν] : ‖∫ (x : ↥Ω), φ ↑x ∂ν‖ ≤ ν.real (Subtype.val ⁻¹' K) * ‖{ toFun := ⇑φ, continuous_toFun := ⋯, map_bounded' := ⋯ }‖

The integral of a test function supported in a compact K ⊆ Ω against a measure on Ω that is finite on compact sets is at most the measure of K times the sup norm.

theorem TestFunction.integrable_bilin_subtype {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} [MeasurableSpace E] [OpensMeasurableSpace E] {F₂ : Type u_3} {F₃ : Type u_4} [NormedAddCommGroup F₂] [NormedSpace ℝ F₂] [NormedAddCommGroup F₃] [NormedSpace ℝ F₃] (B : F →L[ℝ] F₂ →L[ℝ] F₃) {ν : MeasureTheory.Measure ↥Ω} {g : ↥Ω → F₂} (hg : MeasureTheory.LocallyIntegrable g ν) (φ : TestFunction Ω F n) : MeasureTheory.Integrable (fun (x : ↥Ω) => (B (φ ↑x)) (g x)) ν

A test function on Ω pairs integrably, through a continuous bilinear map B, with every function g that is locally integrable for a measure on the subspace Ω.

theorem TestFunction.neg_integral_smul_neg_add_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} [MeasurableSpace E] [OpensMeasurableSpace E] {κ : Type u_3} {κ' : Type u_4} [Fintype κ] [Fintype κ'] {μ : MeasureTheory.Measure E} {f : E → ℝ} {G : κ → κ' → E → ℝ} (φ : TestFunction Ω ℝ ⊤) (hfloc : MeasureTheory.LocallyIntegrableOn f (↑Ω) μ) (hIG : ∀ (i : κ) (j : κ'), MeasureTheory.Integrable (fun (x : E) => φ x • G i j x) μ) : -∫ (x : E), φ x • -(f x + ∑ i : κ, ∑ j : κ', G i j x) ∂μ = ∫ (x : E) in ↑Ω, f x * φ x ∂μ + ∑ i : κ, ∑ j : κ', ∫ (x : E), φ x • G i j x ∂μ

The right-hand side -(f + ∑ᵢⱼ Gᵢⱼ) of a weak derivative equation, with f locally integrable on Ω and each φ Gᵢⱼ integrable, tests against a real test function φ as follows: -∫ φ · -(f + ∑ᵢⱼ Gᵢⱼ) = ∫_Ω f φ + ∑ᵢⱼ ∫ φ Gᵢⱼ. The two index types of the finite sum are independent.

theorem TestFunction.integrable_inner_subtype {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} [MeasurableSpace E] {G : Type u_3} [NormedAddCommGroup G] [InnerProductSpace ℝ G] [OpensMeasurableSpace E] {m : MeasureTheory.Measure ↥Ω} {v : ↥Ω → G} (φ : TestFunction Ω G n) (hv : MeasureTheory.LocallyIntegrable v m) : MeasureTheory.Integrable (fun (x : ↥Ω) => inner ℝ (φ ↑x) (v x)) m

The pairing of a test vector field with a locally integrable field is integrable.

theorem TestFunction.enorm_integral_inner_le_withDensity {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} [MeasurableSpace E] {G : Type u_3} [NormedAddCommGroup G] [InnerProductSpace ℝ G] {U : Set E} (hU : MeasurableSet U) {φ : TestFunction Ω G n} (hφU : tsupport ⇑φ ⊆ U) (hφ : ∀ (x : E), ‖φ x‖ ≤ 1) (m : MeasureTheory.Measure ↥Ω) (v : ↥Ω → G) : ‖∫ (x : ↥Ω), inner ℝ (φ ↑x) (v x) ∂m‖ₑ ≤ (m.withDensity fun (x : ↥Ω) => ‖v x‖ₑ) (Subtype.val ⁻¹' U)

The pairing of a test vector field supported in U and bounded by 1 with a field v is bounded by the mass of the measure |v| m on U.

theorem TestFunction.exists_nonneg_integral_eq_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} [MeasurableSpace E] [FiniteDimensional ℝ E] [OpensMeasurableSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure] {U : Set E} (hU : IsOpen U) (hne : U.Nonempty) (hUΩ : U ⊆ ↑Ω) : ∃ (φ : TestFunction Ω ℝ n), tsupport ⇑φ ⊆ U ∧ (∀ (x : E), 0 ≤ φ x) ∧ ∫ (x : E), φ x ∂μ = 1

There is a nonnegative integral-one test supported in any nonempty open subset of the domain. The measure need not be translation invariant.

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

The directional derivative of a test function has integral zero against an additive Haar measure: ∫ ∂_w φ = 0.