Mass of functionals on vector-valued test functions

For a map f : 𝓓^{n}(Ω, F) → V from F-valued test functions on an open set Ω of a real normed space E to a real normed space V, the mass is the extended supremum

mass f = ⨆ { ‖f φ‖ₑ | φ ∈ 𝓓^{n}(Ω, F), ‖φ x‖ ≤ 1 for all x },

and the local mass localMass f U takes the same supremum over the tests supported in U. With F = E [⋀^Fin k]→L[ℝ] ℝ and V = ℝ, a continuous linear f is a k-current on Ω, the pointwise norm of a test form is the ContinuousAlternatingMap operator norm, and mass f is the extended mass of the current with respect to this norm; it is often infinite. When E is an inner-product space the operator norm on forms is the comass, so mass f is then Federer's mass; this comparison is not proved in this file. A current has locally finite mass when it satisfies an order-zero bound on the tests supported in each compact subset of Ω.

Main declarations

• Distribution.mass, Distribution.localMass: the extended mass and local mass.
• Distribution.enorm_apply_le_localMass_mul: for linear T, ‖T φ‖ₑ ≤ localMass T U * ‖φ‖_∞ when φ is supported in U.
• Distribution.localMass_comp_le_of_enorm_apply_le, Distribution.HasLocallyFiniteMass.comp_of_norm_apply_le: precomposition with a pointwise bounded map of test functions (which does not enlarge supports).
• Distribution.mass_eq_zero_iff: a linear map has mass zero exactly when it vanishes.
• Distribution.localMass_add_localMass_le: for a real-valued linear map, the local masses on disjoint sets add up to at most the local mass on their union.
• Distribution.mass_add_le, Distribution.mass_smul: the triangle inequality and homogeneity.
• Distribution.lowerSemicontinuous_mass: mass is lower semicontinuous for pointwise (weak) convergence; Distribution.mass_le_liminf is the corresponding liminf bound.
• Distribution.mass_comp_monoCLM: the mass of the restriction to an open Ω' ⊆ Ω is the local mass on Ω'; Distribution.localMass_comp_monoCLM gives the local version.
• Distribution.HasLocallyFiniteMass.comp_monoCLM: open restriction preserves local finiteness.
• Distribution.HasLocallyFiniteMass and Distribution.hasLocallyFiniteMass_iff_localMass_ne_top: local finiteness of mass by order-zero bounds and its variational characterization.
• Distribution.mass_apply_apply: the point evaluation φ ↦ ℓ (φ x) has mass ‖ℓ‖; in particular the degree-zero point current has mass one (Distribution.mass_apply_finZero).
• Distribution.mass_integral_apply: integration against a locally integrable field G has mass ∫_Ω ‖G‖.

References

• H. Federer, Geometric Measure Theory, §4.1.7 (the mass of a current).
• L. Simon, Introduction to Geometric Measure Theory, Chapter 6, §2 (currents and their mass).

noncomputable def Distribution.localMass {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} (f : TestFunction Ω F n → V) (U : Set E) : ENNReal

The local mass of f on a set U: the supremum of ‖f φ‖ₑ over the tests φ supported in U with ‖φ x‖ ≤ 1 everywhere.

noncomputable def Distribution.mass {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} (f : TestFunction Ω F n → V) : ENNReal

The (extended) mass of f: the supremum of ‖f φ‖ₑ over the tests φ with ‖φ x‖ ≤ 1 everywhere. With F a space of alternating forms, this is the mass of the current with respect to the operator norm on forms (which is the comass when E is an inner-product space); it may be infinite.

theorem Distribution.enorm_le_localMass {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {f : TestFunction Ω F n → V} {U : Set E} {φ : TestFunction Ω F n} (hφU : tsupport ⇑φ ⊆ U) (hφ : ∀ (x : E), ‖φ x‖ ≤ 1) : ‖f φ‖ₑ ≤ localMass f U

theorem Distribution.enorm_le_mass {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {f : TestFunction Ω F n → V} {φ : TestFunction Ω F n} (hφ : ∀ (x : E), ‖φ x‖ ≤ 1) : ‖f φ‖ₑ ≤ mass f

theorem Distribution.localMass_le_iff {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {f : TestFunction Ω F n → V} {U : Set E} {c : ENNReal} : localMass f U ≤ c ↔ ∀ (φ : TestFunction Ω F n), tsupport ⇑φ ⊆ U → (∀ (x : E), ‖φ x‖ ≤ 1) → ‖f φ‖ₑ ≤ c

theorem Distribution.mass_le_iff {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {f : TestFunction Ω F n → V} {c : ENNReal} : mass f ≤ c ↔ ∀ (φ : TestFunction Ω F n), (∀ (x : E), ‖φ x‖ ≤ 1) → ‖f φ‖ₑ ≤ c

theorem Distribution.localMass_eq_mass_of_subset {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {f : TestFunction Ω F n → V} {U : Set E} (h : ↑Ω ⊆ U) : localMass f U = mass f

The local mass on any set containing Ω is the mass.

@[simp]

theorem Distribution.localMass_univ {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {f : TestFunction Ω F n → V} : localMass f Set.univ = mass f

theorem Distribution.localMass_mono {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {f : TestFunction Ω F n → V} {U U' : Set E} (h : U ⊆ U') : localMass f U ≤ localMass f U'

theorem Distribution.localMass_le_mass {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {f : TestFunction Ω F n → V} {U : Set E} : localMass f U ≤ mass f

@[simp]

theorem Distribution.localMass_zero {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {U : Set E} : localMass 0 U = 0

@[simp]

theorem Distribution.mass_zero {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} : mass 0 = 0

theorem Distribution.localMass_add_le {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {f g : TestFunction Ω F n → V} {U : Set E} : localMass (f + g) U ≤ localMass f U + localMass g U

theorem Distribution.mass_add_le {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {f g : TestFunction Ω F n → V} : mass (f + g) ≤ mass f + mass g

@[simp]

theorem Distribution.localMass_smul {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {f : TestFunction Ω F n → V} {U : Set E} [NormedSpace ℝ V] (a : ℝ) : localMass (a • f) U = ‖a‖ₑ * localMass f U

@[simp]

theorem Distribution.mass_smul {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {f : TestFunction Ω F n → V} [NormedSpace ℝ V] (a : ℝ) : mass (a • f) = ‖a‖ₑ * mass f

@[simp]

theorem Distribution.localMass_neg {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {f : TestFunction Ω F n → V} {U : Set E} : localMass (-f) U = localMass f U

@[simp]

theorem Distribution.mass_neg {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {f : TestFunction Ω F n → V} : mass (-f) = mass f

theorem Distribution.localMass_sub_le {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {f g : TestFunction Ω F n → V} {U : Set E} : localMass (f - g) U ≤ localMass f U + localMass g U

theorem Distribution.mass_sub_le {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {f g : TestFunction Ω F n → V} : mass (f - g) ≤ mass f + mass g

theorem Distribution.mass_sum_le {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {ι : Type u_4} (s : Finset ι) (f : ι → TestFunction Ω F n → V) : mass (∑ i ∈ s, f i) ≤ ∑ i ∈ s, mass (f i)

The mass of a finite sum is at most the sum of the masses.

@[simp]

theorem Distribution.mass_comp_postcompCLM_linearIsometryEquiv {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] (f : TestFunction Ω F n → V) (e : G ≃ₗᵢ[ℝ] F) : mass (f ∘ ⇑(TestFunction.postcompCLM ↑↑e)) = mass f

Changing the values of test functions by a linear isometric equivalence preserves mass.

theorem Distribution.enorm_apply_le_localMass_mul {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {U : Set E} {φ : TestFunction Ω F n} [NormedSpace ℝ V] {𝓕 : Type u_4} [FunLike 𝓕 (TestFunction Ω F n) V] [LinearMapClass 𝓕 ℝ (TestFunction Ω F n) V] (T : 𝓕) (hφU : tsupport ⇑φ ⊆ U) : ‖T φ‖ₑ ≤ localMass (⇑T) U * ‖{ toFun := ⇑φ, continuous_toFun := ⋯, map_bounded' := ⋯ }‖ₑ

The mass bound: a linear map evaluated on a test supported in U is bounded by the local mass on U times the supremum norm of the test.

theorem Distribution.enorm_apply_le_localMass_mul_of_forall_enorm_le {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {U : Set E} {φ : TestFunction Ω F n} {c : ENNReal} [NormedSpace ℝ V] {𝓕 : Type u_4} [FunLike 𝓕 (TestFunction Ω F n) V] [LinearMapClass 𝓕 ℝ (TestFunction Ω F n) V] (T : 𝓕) (hφU : tsupport ⇑φ ⊆ U) (hφc : ∀ (x : E), ‖φ x‖ₑ ≤ c) : ‖T φ‖ₑ ≤ localMass (⇑T) U * c

The mass bound for a test bounded pointwise by c and supported in U.

theorem Distribution.localMass_comp_le_of_enorm_apply_le {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {U : Set E} {c : ENNReal} [NormedSpace ℝ V] {𝓕 : Type u_4} [FunLike 𝓕 (TestFunction Ω F n) V] [LinearMapClass 𝓕 ℝ (TestFunction Ω F n) V] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace ℝ G] (T : 𝓕) {L : TestFunction Ω G n → TestFunction Ω F n} (hLs : ∀ (ψ : TestFunction Ω G n), tsupport ⇑(L ψ) ⊆ tsupport ⇑ψ) {b : E → ENNReal} (hL : ∀ (ψ : TestFunction Ω G n) (x : E), ‖(L ψ) x‖ₑ ≤ b x * ‖ψ x‖ₑ) (hbc : ∀ x ∈ U ∩ ↑Ω, b x ≤ c) : localMass (⇑T ∘ L) U ≤ c * localMass (⇑T) U

Order-zero operators and local mass. If a map L of test functions does not enlarge supports and satisfies ‖L ψ x‖ₑ ≤ b x ‖ψ x‖ₑ with b ≤ c on U ∩ Ω, then precomposition with L multiplies the local mass on U by at most c.

theorem Distribution.enorm_apply_le_mass_mul {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} [NormedSpace ℝ V] {𝓕 : Type u_4} [FunLike 𝓕 (TestFunction Ω F n) V] [LinearMapClass 𝓕 ℝ (TestFunction Ω F n) V] (T : 𝓕) (φ : TestFunction Ω F n) : ‖T φ‖ₑ ≤ mass ⇑T * ‖{ toFun := ⇑φ, continuous_toFun := ⋯, map_bounded' := ⋯ }‖ₑ

theorem Distribution.norm_apply_le_of_mass_le {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} [NormedSpace ℝ V] {𝓕 : Type u_4} [FunLike 𝓕 (TestFunction Ω F n) V] [LinearMapClass 𝓕 ℝ (TestFunction Ω F n) V] (T : 𝓕) {C : NNReal} (hT : mass ⇑T ≤ ↑C) (φ : TestFunction Ω F n) : ‖T φ‖ ≤ ↑C * ‖{ toFun := ⇑φ, continuous_toFun := ⋯, map_bounded' := ⋯ }‖

A finite mass bound controls each evaluation by the supremum norm of the test.

theorem Distribution.mass_eq_zero_iff {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} [NormedSpace ℝ V] {𝓕 : Type u_4} [FunLike 𝓕 (TestFunction Ω F n) V] [LinearMapClass 𝓕 ℝ (TestFunction Ω F n) V] (T : 𝓕) : mass ⇑T = 0 ↔ ⇑T = 0

Mass zero iff current zero.

theorem Distribution.localMass_add_localMass_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {U U' : Set E} {𝓕 : Type u_4} [FunLike 𝓕 (TestFunction Ω F n) ℝ] [LinearMapClass 𝓕 ℝ (TestFunction Ω F n) ℝ] (T : 𝓕) (h : Disjoint U U') : localMass (⇑T) U + localMass (⇑T) U' ≤ localMass (⇑T) (U ∪ U')

On disjoint sets, the local masses of a real-valued linear map add up to at most the local mass on the union.

theorem Distribution.lowerSemicontinuous_localMass {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} (U : Set E) : LowerSemicontinuous fun (f : TestFunction Ω F n → V) => localMass f U

Weak lower semicontinuity of local mass. On the space of maps 𝓓^{n}(Ω, F) → V with the topology of pointwise convergence, the local mass on any set is lower semicontinuous.

theorem Distribution.lowerSemicontinuous_mass {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} : LowerSemicontinuous fun (f : TestFunction Ω F n → V) => mass f

Weak lower semicontinuity of mass.

theorem Distribution.mass_le_liminf {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {f : TestFunction Ω F n → V} {ι : Type u_4} {l : Filter ι} {fs : ι → TestFunction Ω F n → V} (h : ∀ (φ : TestFunction Ω F n), Filter.Tendsto (fun (i : ι) => fs i φ) l (nhds (f φ))) : mass f ≤ Filter.liminf (fun (i : ι) => mass (fs i)) l

If fᵢ φ → f φ along l for every test φ, then mass f ≤ liminf mass fᵢ.

theorem Distribution.mass_comp_monoCLM {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {f : TestFunction Ω F n → V} {Ω' : TopologicalSpace.Opens E} (h : Ω' ≤ Ω) : mass (f ∘ ⇑(TestFunction.monoCLM ℝ)) = localMass f ↑Ω'

Restriction. The mass of the restriction of f to tests on an open Ω' ⊆ Ω is the local mass of f on Ω'.

theorem Distribution.mass_comp_monoCLM_le {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {f : TestFunction Ω F n → V} {Ω' : TopologicalSpace.Opens E} (h : Ω' ≤ Ω) : mass (f ∘ ⇑(TestFunction.monoCLM ℝ)) ≤ mass f

Restriction to an open subset does not increase mass.

theorem Distribution.localMass_comp_monoCLM {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {Ω' : TopologicalSpace.Opens E} (f : TestFunction Ω F n → V) (h : Ω' ≤ Ω) (U : Set E) : localMass (f ∘ ⇑(TestFunction.monoCLM ℝ)) U = localMass f (U ∩ ↑Ω')

The local mass of an open restriction is the local mass on the intersection with its domain. The testing set U need not be open or measurable.

def Distribution.HasLocallyFiniteMass {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} (f : TestFunction Ω F n → V) : Prop

A map on test functions has locally finite mass if it satisfies an order-zero bound on the tests supported in each compact subset of Ω.

theorem Distribution.hasLocallyFiniteMass_def {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {f : TestFunction Ω F n → V} : HasLocallyFiniteMass f ↔ ∀ (K : Set E), IsCompact K → K ⊆ ↑Ω → ∃ (C : ℝ), 0 ≤ C ∧ ∀ (φ : TestFunction Ω F n), tsupport ⇑φ ⊆ K → ‖f φ‖ ≤ C * ‖{ toFun := ⇑φ, continuous_toFun := ⋯, map_bounded' := ⋯ }‖

Unfolding HasLocallyFiniteMass into its order-zero bounds on compact subsets of Ω.

theorem Distribution.HasLocallyFiniteMass.comp_monoCLM {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {Ω' : TopologicalSpace.Opens E} {f : TestFunction Ω F n → V} (hf : HasLocallyFiniteMass f) (h : Ω' ≤ Ω) : HasLocallyFiniteMass (f ∘ ⇑(TestFunction.monoCLM ℝ))

Open restriction preserves locally finite mass, with the same order-zero bound on each compact set in the smaller domain.

theorem Distribution.hasLocallyFiniteMass_zero {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} : HasLocallyFiniteMass 0

theorem Distribution.HasLocallyFiniteMass.add {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {f g : TestFunction Ω F n → V} (hf : HasLocallyFiniteMass f) (hg : HasLocallyFiniteMass g) : HasLocallyFiniteMass (f + g)

theorem Distribution.HasLocallyFiniteMass.neg {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {f : TestFunction Ω F n → V} (hf : HasLocallyFiniteMass f) : HasLocallyFiniteMass (-f)

theorem Distribution.HasLocallyFiniteMass.sub {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {f g : TestFunction Ω F n → V} (hf : HasLocallyFiniteMass f) (hg : HasLocallyFiniteMass g) : HasLocallyFiniteMass (f - g)

theorem Distribution.HasLocallyFiniteMass.smul {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {f : TestFunction Ω F n → V} [NormedSpace ℝ V] (hf : HasLocallyFiniteMass f) (a : ℝ) : HasLocallyFiniteMass (a • f)

theorem Distribution.HasLocallyFiniteMass.comp_of_norm_apply_le {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {T : TestFunction Ω F n → V} (hT : HasLocallyFiniteMass T) {L : TestFunction Ω G n → TestFunction Ω F n} {b : E → ℝ} (hb : Continuous b) (hL : ∀ (ψ : TestFunction Ω G n) (x : E), ‖(L ψ) x‖ ≤ b x * ‖ψ x‖) : HasLocallyFiniteMass (T ∘ L)

Order-zero operators preserve local finiteness. Precomposition with a map L of test functions that satisfies a pointwise bound ‖L ψ x‖ ≤ b x ‖ψ x‖ by a continuous weight b preserves locally finite mass. Such a map does not enlarge supports.

theorem Distribution.hasLocallyFiniteMass_iff_localMass_ne_top {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} [NormedSpace ℝ V] {𝓕 : Type u_4} [FunLike 𝓕 (TestFunction Ω F n) V] [LinearMapClass 𝓕 ℝ (TestFunction Ω F n) V] (T : 𝓕) : HasLocallyFiniteMass ⇑T ↔ ∀ (K : Set E), IsCompact K → K ⊆ ↑Ω → localMass (⇑T) K ≠ ⊤

Variational characterization of local finiteness of mass. A linear map on test functions has locally finite mass if and only if its local mass on every compact subset of Ω is finite.

theorem Distribution.hasLocallyFiniteMass_of_mass_ne_top {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} [NormedSpace ℝ V] {𝓕 : Type u_4} [FunLike 𝓕 (TestFunction Ω F n) V] [LinearMapClass 𝓕 ℝ (TestFunction Ω F n) V] (T : 𝓕) (hT : mass ⇑T ≠ ⊤) : HasLocallyFiniteMass ⇑T

A linear map of finite mass has locally finite mass.

theorem Distribution.HasLocallyFiniteMass.continuous {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} [NormedSpace ℝ V] {L : TestFunction Ω F n →ₗ[ℝ] V} (hL : HasLocallyFiniteMass ⇑L) : Continuous ⇑L

Locally finite mass implies continuity. A linear map on test functions with locally finite mass is continuous for the test-function topology, so it is a distribution of order zero.

theorem Distribution.mass_apply_apply {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} [FiniteDimensional ℝ E] [NormedSpace ℝ V] {x : E} (hx : x ∈ Ω) (ℓ : F →L[ℝ] V) : (mass fun (φ : TestFunction Ω F n) => ℓ (φ x)) = ‖ℓ‖ₑ

Point currents. For x ∈ Ω, the evaluation φ ↦ ℓ (φ x) of a continuous linear map at the value of the test at x has mass ‖ℓ‖.

theorem Distribution.mass_apply_finZero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} [FiniteDimensional ℝ E] {x : E} (hx : x ∈ Ω) : (mass fun (ω : TestFunction Ω (E [⋀^Fin 0]→L[ℝ] ℝ) n) => (ω x) ![]) = 1

The degree-zero point current ω ↦ ω x ![] at a point of Ω has mass one.

theorem Distribution.mass_integral_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {G : E → H →L[ℝ] ℝ} (hG : MeasureTheory.LocallyIntegrableOn G (↑Ω) μ) : (mass fun (φ : TestFunction Ω H ⊤) => ∫ (x : E), (G x) (φ x) ∂μ) = ∫⁻ (x : E) in ↑Ω, ‖G x‖ₑ ∂μ

Mass of an absolutely continuous current. Against an additive Haar measure, integration against a field G of continuous linear functionals on a real Hilbert space, locally integrable on Ω, has mass ∫_Ω ‖G‖; both sides may be infinite.