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]

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.exists_variation_le_add' {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) {ε : ENNReal} (hε : 0 < ε) (hμ : μ.variation s ≠ ⊤) : ∃ (P : Finset (Set X)), (∀ t ∈ P, t ⊆ s) ∧ (↑P).PairwiseDisjoint id ∧ (∀ t ∈ P, MeasurableSet t) ∧ μ.variation s ≤ ∑ p ∈ P, ‖↑μ p‖ₑ + ε

Measure version of preVariation.exists_Finpartition_sum_ge'.

theorem MeasureTheory.VectorMeasure.exists_variation_le_add {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) {ε : NNReal} (hε : 0 < ε) (hμ : μ.variation s ≠ ⊤) : ∃ (P : Finset (Set X)), (∀ t ∈ P, t ⊆ s) ∧ (↑P).PairwiseDisjoint id ∧ (∀ t ∈ P, MeasurableSet t) ∧ μ.variation s ≤ ∑ p ∈ P, ‖↑μ p‖ₑ + ↑ε

Measure version of preVariation.exists_Finpartition_sum_ge.

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_apply_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} {s : Set X} {m : Measure X} (hs : MeasurableSet s) (h : ∀ (E : Set X), MeasurableSet E → E ⊆ s → ‖↑μ E‖ₑ ≤ m E) : μ.variation s ≤ m s

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.variation_apply_eq_zero {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) : μ.variation s = 0 ↔ ∀ t ⊆ s, MeasurableSet t → ↑μ t = 0

@[simp]

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

theorem MeasureTheory.VectorMeasure.variation_restrict {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) : (μ.restrict s).variation = μ.variation.restrict s

theorem MeasureTheory.VectorMeasure.variation_restrict_le {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [TopologicalSpace V] [ENormedAddCommMonoid V] [T2Space V] {μ : VectorMeasure X V} {s : Set X} : (μ.restrict s).variation ≤ μ.variation.restrict s

instance MeasureTheory.VectorMeasure.instIsFiniteMeasureVariationRestrict {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [TopologicalSpace V] [ENormedAddCommMonoid V] [T2Space V] {μ : VectorMeasure X V} {s : Set X} [IsFiniteMeasure μ.variation] : IsFiniteMeasure (μ.restrict s).variation

theorem MeasureTheory.VectorMeasure.variation_map_le {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [TopologicalSpace V] [ENormedAddCommMonoid V] [T2Space V] {μ : VectorMeasure X V} {Y : Type u_3} [MeasurableSpace Y] {φ : X → Y} : (μ.map φ).variation ≤ Measure.map φ μ.variation

instance MeasureTheory.VectorMeasure.instIsFiniteMeasureVariationMap {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [TopologicalSpace V] [ENormedAddCommMonoid V] [T2Space V] {μ : VectorMeasure X V} {Y : Type u_3} [MeasurableSpace Y] {φ : X → Y} [IsFiniteMeasure μ.variation] : IsFiniteMeasure (μ.map φ).variation

theorem MeasurableEmbedding.variation_map {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [TopologicalSpace V] [ENormedAddCommMonoid V] [T2Space V] {μ : MeasureTheory.VectorMeasure X V} {Y : Type u_3} [MeasurableSpace Y] {φ : X → Y} (hφ : MeasurableEmbedding φ) : (μ.map φ).variation = MeasureTheory.Measure.map φ μ.variation

@[simp]

theorem MeasureTheory.VectorMeasure.variation_dirac {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [TopologicalSpace V] [ENormedAddCommMonoid V] [T2Space V] {x : X} {v : V} : (dirac x v).variation = ‖v‖ₑ • Measure.dirac x

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

theorem MeasureTheory.VectorMeasure.variation_smul {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [NormedAddCommGroup V] {μ : VectorMeasure X V} {𝕜 : Type u_3} [NormedField 𝕜] [NormedSpace 𝕜 V] {c : 𝕜} : (c • μ).variation = ‖c‖₊ • μ.variation

instance MeasureTheory.VectorMeasure.instIsFiniteMeasureVariationHSMul {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [NormedAddCommGroup V] {μ : VectorMeasure X V} {𝕜 : Type u_3} [NormedField 𝕜] [NormedSpace 𝕜 V] {c : 𝕜} [IsFiniteMeasure μ.variation] : IsFiniteMeasure (c • μ).variation

instance MeasureTheory.VectorMeasure.instIsFiniteMeasureVariationOfFinite {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [NormedAddCommGroup V] {μ : VectorMeasure X V} [Finite X] : IsFiniteMeasure μ.variation

instance MeasureTheory.VectorMeasure.instIsFiniteMeasureVariationDirac {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [NormedAddCommGroup V] {x : X} {v : V} : IsFiniteMeasure (dirac x v).variation

@[simp]

theorem MeasureTheory.VectorMeasure.variation_toSignedMeasure {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} [IsFiniteMeasure μ] : variation μ.toSignedMeasure = μ