The semivariation of a vector measure

The semivariation of a vector measure is the supremum of the variations of its push-forwards to ℝ through all linear forms of norm at most 1. The interest of this notion is that, in the reals, any set has nonnegative or nonpositive measure, so that the variation is realized by a subset (up to a factor of at most 2). This property is inherited by the semivariation in general: one has the inequalities

‖μ s‖ₑ ≤ μ.semivariation s ≤ 2 sup_{t ⊆ s} ‖μ t‖ₑ

The notion of semivariation can in particular be used to show that any vector measure is bounded: there exists C < ∞ such that ‖μ s‖ ≤ C for all s.

Main results

• μ.semivariation: the semivariation of the vector measure μ.
• exists_subset_lt_enorm_apply_of_lt_semivariation: given s, there exists t ⊆ s such that μ.semivariation s ≤ 2 ‖μ t‖ₑ up to an arbitrarily small error.
• μ.bound: the semivariation of univ, in ℝ≥0. It is finite by definition.
• enorm_apply_le_bound: the inequality ‖μ s‖ₑ ≤ μ.bound, uniformly in s.

References

• J. Diestel and J.J. Uhl, Vector Measures

noncomputable def MeasureTheory.VectorMeasure.semivariation {X : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {mX : MeasurableSpace X} (μ : VectorMeasure X E) (s : Set X) : ENNReal

The semivariation of a vector measure, defined as the supremum of the variations of the images of the vector measures under continuous linear forms of norm at most 1.

Equations

• μ.semivariation s = ⨆ ℓ ∈ {ℓ : StrongDual ℝ E | ‖ℓ‖ₑ ≤ 1}, (μ.mapRange ↑ℓ ⋯).variation s

theorem MeasureTheory.VectorMeasure.semivariation_union_le {X : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {mX : MeasurableSpace X} {μ : VectorMeasure X E} {s t : Set X} : μ.semivariation (s ∪ t) ≤ μ.semivariation s + μ.semivariation t

theorem MeasureTheory.VectorMeasure.semivariation_mono {X : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {mX : MeasurableSpace X} {μ : VectorMeasure X E} {s t : Set X} (hst : s ⊆ t) : μ.semivariation s ≤ μ.semivariation t

theorem MeasureTheory.VectorMeasure.semivariation_le_variation {X : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {mX : MeasurableSpace X} {μ : VectorMeasure X E} {s : Set X} : μ.semivariation s ≤ μ.variation s

theorem MeasureTheory.VectorMeasure.enorm_apply_le_semivariation {X : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {mX : MeasurableSpace X} {μ : VectorMeasure X E} {s : Set X} : ‖μ s‖ₑ ≤ μ.semivariation s

theorem MeasureTheory.VectorMeasure.enorm_apply_le_semivariation_of_subset {X : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {mX : MeasurableSpace X} {μ : VectorMeasure X E} {s t : Set X} (hst : s ⊆ t) : ‖μ s‖ₑ ≤ μ.semivariation t

theorem MeasureTheory.VectorMeasure.exists_subset_lt_enorm_apply_of_lt_semivariation {X : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {mX : MeasurableSpace X} {μ : VectorMeasure X E} {s : Set X} (hs : MeasurableSet s) {a : ENNReal} (ha : a < μ.semivariation s) : ∃ t ⊆ s, MeasurableSet t ∧ a < 2 * ‖μ t‖ₑ

noncomputable def MeasureTheory.VectorMeasure.bound {X : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {mX : MeasurableSpace X} (μ : VectorMeasure X E) : NNReal

A constant bounding the norm of μ s for any set s.

Equations

• μ.bound = (μ.semivariation Set.univ).toNNReal

theorem MeasureTheory.VectorMeasure.semivariation_apply_le_bound {X : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {mX : MeasurableSpace X} {μ : VectorMeasure X E} {s : Set X} : μ.semivariation s ≤ ↑μ.bound

theorem MeasureTheory.VectorMeasure.enorm_apply_le_bound {X : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {mX : MeasurableSpace X} {μ : VectorMeasure X E} {s : Set X} : ‖μ s‖ₑ ≤ ↑μ.bound

theorem MeasureTheory.VectorMeasure.nnnorm_apply_le_bound {X : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {mX : MeasurableSpace X} {μ : VectorMeasure X E} {s : Set X} : ‖μ s‖₊ ≤ μ.bound

theorem MeasureTheory.VectorMeasure.norm_apply_le_bound {X : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {mX : MeasurableSpace X} {μ : VectorMeasure X E} {s : Set X} : ‖μ s‖ ≤ ↑μ.bound