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

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

theorem MeasureTheory.VectorMeasure.variation_le_of_forall_enorm_le {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [TopologicalSpace V] [ENormedAddCommMonoid V] [T2Space V] {μ : VectorMeasure X V} {m : Measure X} (h : ∀ (E : Set X), MeasurableSet E → ‖↑μ E‖ₑ ≤ m E) : μ.variation ≤ m

theorem MeasureTheory.VectorMeasure.variation_add_le {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [TopologicalSpace V] [ENormedAddCommMonoid V] [T2Space V] {μ ν : VectorMeasure X V} [ContinuousAdd V] : (μ + ν).variation ≤ μ.variation + ν.variation

theorem MeasureTheory.VectorMeasure.variation_finsetSum_le {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [TopologicalSpace V] [ENormedAddCommMonoid V] [T2Space V] [ContinuousAdd V] {ι : Type u_3} (s : Finset ι) (μ : ι → VectorMeasure X V) : (∑ i ∈ s, μ i).variation ≤ ∑ i ∈ s, (μ i).variation

theorem MeasureTheory.VectorMeasure.norm_measure_le_variation {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [NormedAddCommGroup V] {μ : VectorMeasure X V} {E : Set X} (hE : μ.variation E ≠ ⊤ := by finiteness) : ‖↑μ E‖ ≤ μ.variation.real E

@[simp]

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

theorem MeasureTheory.VectorMeasure.variation_sub_le {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [NormedAddCommGroup V] {μ ν : VectorMeasure X V} : (μ - ν).variation ≤ μ.variation + ν.variation