The content of a set function on open sets

Let Ω be an open set of a Hausdorff space X and let m assign a value in [0, ∞] to every open set of X. Suppose that m is monotone, subadditive and additive on disjoint pairs of open subsets of Ω, and finite on a neighbourhood of every compact subset of Ω. Then its outer approximation K ↦ inf { m V | K ⊆ V ⊆ Ω, V open } on the compact subsets of Ω is a MeasureTheory.Content (TauCeti.contentOfOpens). The value of the induced measure on an open set U is m U as soon as m U is approximated from inside by compact sets (TauCeti.contentOfOpens_measure_preimage_coe).

This is the De Giorgi–Letta criterion in the form of Mathlib's contents. It is the common step of the constructions of measures from functionals: the variation measure of a function of locally bounded variation and the mass measure of a current of locally finite mass.

Main declarations

• TauCeti.opensInf m Ω K: the outer approximation of m on a set K of Ω.
• TauCeti.contentOfOpens: the content on Ω given by the outer approximation of m.
• TauCeti.contentOfOpens_measure_preimage_coe: its measure agrees with m on open sets which are approximated from inside by compact sets.

References

• L. Ambrosio, N. Fusco, D. Pallara, Functions of Bounded Variation and Free Discontinuity Problems, §1.5 (the De Giorgi–Letta criterion).

noncomputable def TauCeti.opensInf {X : Type u_1} [TopologicalSpace X] (m : TopologicalSpace.Opens X → ENNReal) (Ω : TopologicalSpace.Opens X) (K : Set ↥Ω) : ENNReal

The outer approximation of a set function m on open sets at a set K of Ω: the infimum of m V over the open sets V ⊆ Ω containing K.

theorem TauCeti.opensInf_le {X : Type u_1} [TopologicalSpace X] {m : TopologicalSpace.Opens X → ENNReal} {Ω V : TopologicalSpace.Opens X} {K : Set ↥Ω} (hKV : Subtype.val '' K ⊆ ↑V) (hV : V ≤ Ω) : opensInf m Ω K ≤ m V

theorem TauCeti.le_opensInf {X : Type u_1} [TopologicalSpace X] {m : TopologicalSpace.Opens X → ENNReal} {Ω : TopologicalSpace.Opens X} {K : Set ↥Ω} {c : ENNReal} (h : ∀ (V : TopologicalSpace.Opens X), Subtype.val '' K ⊆ ↑V → V ≤ Ω → c ≤ m V) : c ≤ opensInf m Ω K

theorem TauCeti.opensInf_mono {X : Type u_1} [TopologicalSpace X] {m : TopologicalSpace.Opens X → ENNReal} {Ω : TopologicalSpace.Opens X} {K₁ K₂ : Set ↥Ω} (h : K₁ ⊆ K₂) : opensInf m Ω K₁ ≤ opensInf m Ω K₂

theorem TauCeti.opensInf_ne_top {X : Type u_1} [TopologicalSpace X] {m : TopologicalSpace.Opens X → ENNReal} {Ω : TopologicalSpace.Opens X} (hmono : Monotone m) (hfin : ∀ (K : Set X), IsCompact K → K ⊆ ↑Ω → ∃ (U : TopologicalSpace.Opens X), K ⊆ ↑U ∧ m U ≠ ⊤) {K : Set ↥Ω} (hK : IsCompact K) : opensInf m Ω K ≠ ⊤

The outer approximation of m is finite on compact sets if m is finite on a neighbourhood of every compact subset of Ω.

theorem TauCeti.opensInf_union_le {X : Type u_1} [TopologicalSpace X] {m : TopologicalSpace.Opens X → ENNReal} {Ω : TopologicalSpace.Opens X} (hsub : ∀ (U V : TopologicalSpace.Opens X), U ≤ Ω → V ≤ Ω → m (U ⊔ V) ≤ m U + m V) (K₁ K₂ : Set ↥Ω) : opensInf m Ω (K₁ ∪ K₂) ≤ opensInf m Ω K₁ + opensInf m Ω K₂

The outer approximation of a subadditive set function is subadditive.

theorem TauCeti.opensInf_add_le_union {X : Type u_1} [TopologicalSpace X] {m : TopologicalSpace.Opens X → ENNReal} {Ω : TopologicalSpace.Opens X} [T2Space X] (hmono : Monotone m) (hadd : ∀ (U V : TopologicalSpace.Opens X), U ≤ Ω → V ≤ Ω → Disjoint U V → m U + m V ≤ m (U ⊔ V)) {K₁ K₂ : Set ↥Ω} (hK₁ : IsCompact K₁) (hK₂ : IsCompact K₂) (h : Disjoint K₁ K₂) : opensInf m Ω K₁ + opensInf m Ω K₂ ≤ opensInf m Ω (K₁ ∪ K₂)

The outer approximation of a set function which is additive on disjoint open sets is superadditive on disjoint compact sets, since these are separated by disjoint open sets.

noncomputable def TauCeti.contentOfOpens {X : Type u_1} [TopologicalSpace X] {m : TopologicalSpace.Opens X → ENNReal} {Ω : TopologicalSpace.Opens X} [T2Space X] (hmono : Monotone m) (hsub : ∀ (U V : TopologicalSpace.Opens X), U ≤ Ω → V ≤ Ω → m (U ⊔ V) ≤ m U + m V) (hadd : ∀ (U V : TopologicalSpace.Opens X), U ≤ Ω → V ≤ Ω → Disjoint U V → m U + m V ≤ m (U ⊔ V)) (hfin : ∀ (K : Set X), IsCompact K → K ⊆ ↑Ω → ∃ (U : TopologicalSpace.Opens X), K ⊆ ↑U ∧ m U ≠ ⊤) : MeasureTheory.Content ↥Ω

The content on the compact subsets of Ω given by the outer approximation opensInf m Ω of a monotone set function m on open sets which is subadditive, additive on disjoint pairs of open subsets of Ω, and finite on a neighbourhood of every compact subset of Ω.

theorem TauCeti.contentOfOpens_apply {X : Type u_1} [TopologicalSpace X] {m : TopologicalSpace.Opens X → ENNReal} {Ω : TopologicalSpace.Opens X} [T2Space X] (hmono : Monotone m) (hsub : ∀ (U V : TopologicalSpace.Opens X), U ≤ Ω → V ≤ Ω → m (U ⊔ V) ≤ m U + m V) (hadd : ∀ (U V : TopologicalSpace.Opens X), U ≤ Ω → V ≤ Ω → Disjoint U V → m U + m V ≤ m (U ⊔ V)) (hfin : ∀ (K : Set X), IsCompact K → K ⊆ ↑Ω → ∃ (U : TopologicalSpace.Opens X), K ⊆ ↑U ∧ m U ≠ ⊤) (K : TopologicalSpace.Compacts ↥Ω) : (contentOfOpens hmono hsub hadd hfin) K = opensInf m Ω ↑K

theorem TauCeti.contentOfOpens_measure_preimage_coe {X : Type u_1} [TopologicalSpace X] {m : TopologicalSpace.Opens X → ENNReal} {Ω : TopologicalSpace.Opens X} [T2Space X] (hmono : Monotone m) (hsub : ∀ (U V : TopologicalSpace.Opens X), U ≤ Ω → V ≤ Ω → m (U ⊔ V) ≤ m U + m V) (hadd : ∀ (U V : TopologicalSpace.Opens X), U ≤ Ω → V ≤ Ω → Disjoint U V → m U + m V ≤ m (U ⊔ V)) (hfin : ∀ (K : Set X), IsCompact K → K ⊆ ↑Ω → ∃ (U : TopologicalSpace.Opens X), K ⊆ ↑U ∧ m U ≠ ⊤) [MeasurableSpace X] [BorelSpace X] {U : TopologicalSpace.Opens X} (hinner : m U ≤ ⨆ (K : TopologicalSpace.Compacts ↥Ω), ⨆ (_ : ↑K ⊆ Subtype.val ⁻¹' ↑U), opensInf m Ω ↑K) : (contentOfOpens hmono hsub hadd hfin).measure (Subtype.val ⁻¹' ↑U) = m U

The measure of an open set. The measure induced by contentOfOpens gives an open set U of X the value m U, provided m U is approximated from inside by the outer approximations of the compact subsets of Ω ∩ U.