Properties of variation

We prove basic properties of variation for μ : VectorMeasure X V in ENormedAddCommMonoid V on MeasurableSpace X. It is defined as the supremum over partitions {Eᵢ} of E, of the quantity ∑ᵢ, ‖μ(Eᵢ)‖. This definition allows one to define the integral against such vector-valued measures.

Main results

• enorm_measure_le_variation: ‖μ E‖ₑ ≤ variation μ E.
• variation_zero: (0 : VectorMeasure X V).variation = 0.
• variation_neg: (-μ).variation = μ.variation.
• absolutelyContinuous: μ ≪ᵥ μ.variation.

References

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

@[simp]

theorem MeasureTheory.VectorMeasure.variation_apply {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [TopologicalSpace V] [ENormedAddCommMonoid V] [T2Space V] (μ : VectorMeasure X V) (s : Set X) : μ.variation s = (preVariation (fun (x : Set X) => ‖↑μ x‖ₑ) ⋯ ⋯) s

@[simp]

theorem MeasureTheory.VectorMeasure.ennrealVariation_apply {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [TopologicalSpace V] [ENormedAddCommMonoid V] [T2Space V] (μ : VectorMeasure X V) {s : Set X} (hs : MeasurableSet s) : ↑μ.ennrealVariation s = μ.variation s

theorem MeasureTheory.VectorMeasure.le_variation {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [TopologicalSpace V] [ENormedAddCommMonoid V] [T2Space V] (μ : VectorMeasure X V) {s : Set X} (hs : MeasurableSet s) {P : Finset (Set X)} (hP₁ : ∀ t ∈ P, t ⊆ s) (hP₂ : (↑P).PairwiseDisjoint id) : ∑ p ∈ P, ‖↑μ p‖ₑ ≤ μ.variation s

Measure version of sum_le_preVariationFun_of_subset.

theorem MeasureTheory.VectorMeasure.enorm_measure_le_variation {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [TopologicalSpace V] [ENormedAddCommMonoid V] [T2Space V] (μ : VectorMeasure X V) (E : Set X) : ‖↑μ E‖ₑ ≤ μ.variation E

@[simp]

theorem MeasureTheory.VectorMeasure.variation_zero {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [TopologicalSpace V] [ENormedAddCommMonoid V] [T2Space V] : variation 0 = 0

@[simp]

theorem MeasureTheory.VectorMeasure.variation_neg {X : Type u_1} {mX : MeasurableSpace X} {V : Type u_3} [NormedAddCommGroup V] (μ : VectorMeasure X V) : (-μ).variation = μ.variation

theorem MeasureTheory.VectorMeasure.absolutelyContinuous {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [TopologicalSpace V] [ENormedAddCommMonoid V] [T2Space V] (μ : VectorMeasure X V) : μ.AbsolutelyContinuous μ.ennrealVariation