Pre-variation of a subadditive set function

Given a σ-subadditive ℝ≥0∞-valued set function f, we define the pre-variation as the supremum over finite measurable partitions of the sum of f on the parts. This construction yields a measure.

Main definitions

• IsSigmaSubadditiveSetFun f — f is σ-subadditive on measurable sets
• ennrealPreVariation f — the VectorMeasure X ℝ≥0∞ built from a σ-subadditive function
• preVariation f — the Measure X built from a σ-subadditive function

References

• [Walter Rudin, Real and Complex Analysis.][Rud87]

Pre-variation of a subadditive ℝ≥0∞-valued function

Given a set function f : Set X → ℝ≥0∞ we can define another set function by taking the supremum over all finite partitions of measurable sets E i of the sum of ∑ i, f (E i). If f is σ-subadditive then the function defined is an ℝ≥0∞-valued measure.

noncomputable def MeasureTheory.preVariationFun {X : Type u_1} [MeasurableSpace X] (f : Set X → ENNReal) (s : Set X) : ENNReal

If s is measurable then preVariationFun f s is the supremum over partitions P of s of the quantity ∑ p ∈ P.parts, f p. If s is not measurable then it is set to 0.

Equations

• MeasureTheory.preVariationFun f s = if h : MeasurableSet s then ⨆ (P : Finpartition ⟨s, h⟩), ∑ p ∈ P.parts, f ↑p else 0

theorem MeasureTheory.preVariation.empty {X : Type u_1} [MeasurableSpace X] (f : Set X → ENNReal) : preVariationFun f ∅ = 0

preVariationFun of the empty set is equal to zero.

theorem MeasureTheory.preVariation.sum_le {X : Type u_1} [MeasurableSpace X] (f : Set X → ENNReal) {s : Set X} (hs : MeasurableSet s) (P : Finpartition ⟨s, hs⟩) : ∑ p ∈ P.parts, f ↑p ≤ preVariationFun f s

theorem MeasureTheory.preVariation.sum_le_preVariationFun_of_subset {X : Type u_1} [MeasurableSpace X] (f : Set X → ENNReal) {s₁ s₂ : Set X} (hs₁ : MeasurableSet s₁) (hs₂ : MeasurableSet s₂) (h : s₁ ⊆ s₂) (P : Finpartition ⟨s₁, hs₁⟩) : ∑ p ∈ P.parts, f ↑p ≤ preVariationFun f s₂

If P is a partition of s₁ and s₁ ⊆ s₂ then ∑ p ∈ P.parts, f p ≤ preVariationFun f s₂.

theorem MeasureTheory.preVariation.mono {X : Type u_1} [MeasurableSpace X] (f : Set X → ENNReal) {s₁ s₂ : Set X} (hs₂ : MeasurableSet s₂) (h : s₁ ⊆ s₂) : preVariationFun f s₁ ≤ preVariationFun f s₂

preVariationFun is monotone in terms of the (measurable) set.

theorem MeasureTheory.preVariation.exists_Finpartition_sum_gt {X : Type u_1} [MeasurableSpace X] (f : Set X → ENNReal) {s : Set X} (hs : MeasurableSet s) {a : ENNReal} (ha : a < preVariationFun f s) : ∃ (P : Finpartition ⟨s, hs⟩), a < ∑ p ∈ P.parts, f ↑p

theorem MeasureTheory.preVariation.exists_Finpartition_sum_ge {X : Type u_1} [MeasurableSpace X] (f : Set X → ENNReal) {s : Set X} (hs : MeasurableSet s) {ε : NNReal} (hε : 0 < ε) (h : preVariationFun f s ≠ ⊤) : ∃ (P : Finpartition ⟨s, hs⟩), preVariationFun f s ≤ ∑ p ∈ P.parts, f ↑p + ↑ε

theorem MeasureTheory.preVariation.Finset.sup_measurableSetSubtype_eq_biUnion {X : Type u_1} [MeasurableSpace X] {ι : Type u_2} (s : ι → Subtype MeasurableSet) (I : Finset ι) : ↑(I.sup s) = ⋃ i ∈ I, ↑(s i)

The sup of measurable set subtypes over a finset equals the biUnion of the underlying sets.

theorem MeasureTheory.preVariation.sum_le_preVariationFun_iUnion' {X : Type u_1} [MeasurableSpace X] (f : Set X → ENNReal) {s : ℕ → Set X} (hs : ∀ (i : ℕ), MeasurableSet (s i)) (hs' : Pairwise (Function.onFun Disjoint s)) (P : (i : ℕ) → Finpartition ⟨s i, ⋯⟩) (n : ℕ) : ∑ i ∈ Finset.range n, ∑ p ∈ (P i).parts, f ↑p ≤ preVariationFun f (⋃ (i : ℕ), s i)

theorem MeasureTheory.preVariation.sum_le_preVariationFun_iUnion {X : Type u_1} [MeasurableSpace X] (f : Set X → ENNReal) {s : ℕ → Set X} (hs : ∀ (i : ℕ), MeasurableSet (s i)) (hs' : Pairwise (Function.onFun Disjoint s)) : ∑' (i : ℕ), preVariationFun f (s i) ≤ preVariationFun f (⋃ (i : ℕ), s i)

def MeasureTheory.IsSigmaSubadditiveSetFun {X : Type u_1} [MeasurableSpace X] (f : Set X → ENNReal) : Prop

A set function is σ-subadditive on measurable sets if the value assigned to the union of a countable disjoint family of measurable sets is bounded above by the sum of values on the family.

Equations

• MeasureTheory.IsSigmaSubadditiveSetFun f = ∀ (s : ℕ → { t : Set X // MeasurableSet t }), Pairwise (Function.onFun Disjoint (Subtype.val ∘ s)) → f (⋃ (i : ℕ), ↑(s i)) ≤ ∑' (i : ℕ), f ↑(s i)

theorem MeasureTheory.preVariation.iUnion {X : Type u_1} [MeasurableSpace X] {f : Set X → ENNReal} (hf : IsSigmaSubadditiveSetFun f) (hf' : f ∅ = 0) (s : ℕ → Set X) (hs : ∀ (i : ℕ), MeasurableSet (s i)) (hs' : Pairwise (Function.onFun Disjoint s)) : HasSum (fun (i : ℕ) => preVariationFun f (s i)) (preVariationFun f (⋃ (i : ℕ), s i))

Additivity of preVariationFun for disjoint measurable sets.

Construction of measures from σ-subadditive functions

noncomputable def MeasureTheory.ennrealPreVariation {X : Type u_1} [MeasurableSpace X] (f : Set X → ENNReal) (hf : IsSigmaSubadditiveSetFun f) (hf' : f ∅ = 0) : VectorMeasure X ENNReal

The VectorMeasure X ℝ≥0∞ built from a σ-subadditive function.

Equations

• MeasureTheory.ennrealPreVariation f hf hf' = { measureOf' := MeasureTheory.preVariationFun f, empty' := ⋯, not_measurable' := ⋯, m_iUnion' := ⋯ }

noncomputable def MeasureTheory.preVariation {X : Type u_1} [MeasurableSpace X] (f : Set X → ENNReal) (hf : IsSigmaSubadditiveSetFun f) (hf' : f ∅ = 0) : Measure X

The Measure X built from a σ-subadditive function.

Equations

• MeasureTheory.preVariation f hf hf' = (MeasureTheory.ennrealPreVariation f hf hf').ennrealToMeasure