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.
• ennrealVariation_eq_self: if μ : VectorMeasure X ℝ≥0∞ then μ.ennrealVariation = μ.

References

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

theorem MeasureTheory.VectorMeasure.sum_finpartition {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [AddCommMonoid V] [TopologicalSpace V] [T2Space V] (μ : VectorMeasure X V) {s : Set X} {hs : MeasurableSet s} (P : Finpartition ⟨s, hs⟩) : ∑ p ∈ P.parts, μ ↑p = μ s

The sum of a vector measure μ on a Finpartition of Subtype MeasurableSet equals μ s.

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_lt_sum_of_lt_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) {a : ENNReal} (ha : a < μ.variation s) : ∃ (P : Finset (Set X)), (∀ t ∈ P, t ⊆ s) ∧ (↑P).PairwiseDisjoint id ∧ (∀ t ∈ P, MeasurableSet t) ∧ a < ∑ p ∈ P, ‖μ p‖ₑ

Measure version of preVariation.exists_Finpartition_sum_gt.

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.Measure.variation_toSignedMeasure {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} [IsFiniteMeasure μ] : VectorMeasure.variation μ.toSignedMeasure = μ

theorem MeasureTheory.SignedMeasure.exists_subset_lt_enorm_apply_of_lt_variation {X : Type u_1} {mX : MeasurableSpace X} (μ : SignedMeasure X) {s : Set X} (hs : MeasurableSet s) {a : ENNReal} (ha : a < (VectorMeasure.variation μ) s) : ∃ t ⊆ s, MeasurableSet t ∧ a < 2 * ‖μ t‖ₑ

For a signed measure, the variation is realized by the norm of the measure of a single set, up to a factor of 2 and an arbitrarily small error.

@[simp]

theorem MeasureTheory.VectorMeasure.iSup_sum_finpartition_parts {X : Type u_1} {mX : MeasurableSpace X} (μ : VectorMeasure X ENNReal) {s : Set X} (hs : MeasurableSet s) : ⨆ (P : Finpartition ⟨s, hs⟩), ∑ p ∈ P.parts, μ ↑p = μ s

For μ : VectorMeasure X ℝ≥0∞ and measurable s, the supremum over Finpartitions of ⟨s, hs⟩ : Subtype MeasurableSet of the sum of μ over parts equals μ s.

theorem MeasureTheory.VectorMeasure.preVariationFun_apply_of_ennreal {X : Type u_1} {mX : MeasurableSpace X} (μ : VectorMeasure X ENNReal) (s : Set X) : preVariationFun (⇑μ) s = μ s

For μ : VectorMeasure X ℝ≥0∞, preVariationFun μ s = μ s for any s.

theorem MeasureTheory.VectorMeasure.variation_eq_ennrealToMeasure {X : Type u_1} {mX : MeasurableSpace X} (μ : VectorMeasure X ENNReal) : μ.variation = μ.ennrealToMeasure

@[simp]

theorem MeasureTheory.VectorMeasure.ennrealVariation_eq_self {X : Type u_1} {mX : MeasurableSpace X} (μ : VectorMeasure X ENNReal) : μ.ennrealVariation = μ