[Merged by Bors] - feat: more API for the variation of vector measures

Mathlib/Data/ENNReal/Action.lean

@@ -104,6 +104,12 @@ instance : PosSMulStrictMono ℝ≥0 ℝ≥0∞ where
 instance : SMulPosMono ℝ≥0 ℝ≥0∞ where
   smul_le_smul_of_nonneg_right _r _ _a _b hab := _root_.mul_le_mul_left (coe_le_coe.2 hab) _
 
+instance : CovariantClass ℝ≥0∞ ℝ≥0∞ (· • ·) (· ≤ ·) :=
+  inferInstanceAs <| CovariantClass ℝ≥0∞ ℝ≥0∞ (· * ·) (· ≤ ·)
+
+instance : CovariantClass ℝ≥0 ℝ≥0∞ (· • ·) (· ≤ ·) :=
+  ⟨fun x x y hxy ↦ by simpa [ENNReal.smul_def] using mul_le_mul_right hxy _⟩
+
 end Actions
 
 end ENNReal

Mathlib/MeasureTheory/Measure/MeasureSpace.lean

@@ -1079,6 +1079,12 @@ protected theorem le_add_left (h : μ ≤ ν) : μ ≤ ν' + ν := fun s => le_a
 
 protected theorem le_add_right (h : μ ≤ ν) : μ ≤ ν + ν' := fun s => le_add_right (h s)
 
+instance [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] [CovariantClass R ℝ≥0∞ (· • ·) (· ≤ ·)] :
+    CovariantClass R (Measure α) (· • ·) (· ≤ ·) where
+  elim c μ ν hμν s := by
+    simp only [smul_apply]
+    gcongr
+
 section sInf
 
 variable {m : Set (Measure α)}
@@ -1494,3 +1500,5 @@ end
 end MeasureTheory
 
 end
+
+set_option linter.style.longFile 1700

Mathlib/MeasureTheory/VectorMeasure/Basic.lean

@@ -408,6 +408,10 @@ def dirac (x : β) (v : M) : VectorMeasure β M where
 @[simp] lemma dirac_apply_of_notMem (hx : x ∉ s) : dirac x v s = 0 := by
   simp [dirac, hx]
 
+@[simp] lemma dirac_zero : dirac x (0 : M) = 0 := by
+  ext s hs
+  simp [dirac]
+
 end Dirac
 
 end VectorMeasure
@@ -631,25 +635,30 @@ end ContinuousAdd
 section Module
 
 variable {R : Type*} [Semiring R] [Module R M] [Module R N]
-variable [ContinuousAdd M] [ContinuousAdd N] [ContinuousConstSMul R M] [ContinuousConstSMul R N]
+
+variable [ContinuousConstSMul R M] [ContinuousConstSMul R N]
+
+@[simp]
+theorem mapRange_smul {v : VectorMeasure α M} {f : M →ₗ[R] N} (hf : Continuous f) {c : R} :
+    (c • v).mapRange f.toAddMonoidHom hf = c • (v.mapRange f.toAddMonoidHom hf) := by
+  ext; simp
+
+variable [ContinuousAdd M] [ContinuousAdd N]
 
 /-- Given a continuous linear map `f : M → N`, `mapRangeₗ` is the linear map mapping the
 vector measure `v` on `M` to the vector measure `f ∘ v` on `N`. -/
 def mapRangeₗ (f : M →ₗ[R] N) (hf : Continuous f) : VectorMeasure α M →ₗ[R] VectorMeasure α N where
   toFun v := v.mapRange f.toAddMonoidHom hf
   map_add' _ _ := mapRange_add hf
-  map_smul' := by
-    intros
-    ext
-    simp
+  map_smul' _ _ := mapRange_smul hf
 
 end Module
 
 end
 
 open Classical in
 /-- The restriction of a vector measure on some set. -/
-def restrict (v : VectorMeasure α M) (i : Set α) : VectorMeasure α M :=
+@[no_expose] def restrict (v : VectorMeasure α M) (i : Set α) : VectorMeasure α M :=
   if hi : MeasurableSet i then
     { measureOf' := fun s => if MeasurableSet s then v (s ∩ i) else 0
       empty' := by simp
@@ -690,6 +699,39 @@ theorem restrict_zero {i : Set α} : (0 : VectorMeasure α M).restrict i = 0 :=
     rw [restrict_apply 0 hi hj, zero_apply, zero_apply]
   · exact dif_neg hi
 
+theorem restrict_dirac {s : Set α} {x : α} {m : M} (hs : MeasurableSet s) [Decidable (x ∈ s)] :
+    (dirac x m).restrict s = if x ∈ s then dirac x m else 0 := by
+  classical
+  ext t ht
+  simp only [hs, ht, restrict_apply]
+  split_ifs with has <;> simp [dirac, ht, ht.inter hs, has]
+
+@[simp]
+theorem restrict_dirac_of_mem {s : Set α} {x : α} {m : M} (hs : MeasurableSet s) (hx : x ∈ s) :
+    (dirac x m).restrict s = dirac x m := by
+  classical
+  simp [restrict_dirac, hs, hx]
+
+@[simp]
+theorem restrict_dirac_of_notMem {s : Set α} {x : α} {m : M} (hx : x ∉ s) :
+    (dirac x m).restrict s = 0 := by
+  classical
+  by_cases hs : MeasurableSet s
+  · simp [restrict_dirac, hs, hx]
+  · simp [restrict, hs]
+
+@[simp]
+theorem restrict_singleton {a : α} : v.restrict {a} = dirac a (v {a}) := by
+  by_cases h : MeasurableSet {a}
+  · ext s hs
+    by_cases ha : a ∈ s <;> simp [*, restrict_apply]
+  · simp [restrict, h]
+
+theorem restrict_restrict {s t : Set α} (hs : MeasurableSet s) (ht : MeasurableSet t) :
+    (v.restrict t).restrict s = v.restrict (s ∩ t) := by
+  ext u hu
+  simp [restrict_apply, hs, hu, ht, Set.inter_assoc]
+
 section ContinuousAdd
 
 variable [ContinuousAdd M]
@@ -727,7 +769,7 @@ end ContinuousAdd
 section Partition
 
 variable {M : Type*} [TopologicalSpace M] [AddCommMonoid M] [T2Space M] [ContinuousAdd M]
-variable (v : VectorMeasure α M) {i : Set α}
+variable {v : VectorMeasure α M} {i s t : Set α}
 
 @[simp]
 theorem restrict_add_restrict_compl (hi : MeasurableSet i) :
@@ -738,6 +780,23 @@ theorem restrict_add_restrict_compl (hi : MeasurableSet i) :
   · simp
   · exact disjoint_compl_right.inter_right' A |>.inter_left' A
 
+theorem restrict_inter_add_diff (hs : MeasurableSet s) (ht : MeasurableSet t) :
+    v.restrict (s ∩ t) + v.restrict (s \ t) = v.restrict s := by
+  ext u hu
+  simp only [add_apply, restrict_apply, hs, hu, hs.inter ht, hs.diff ht]
+  rw [← of_union (by grind) (hu.inter (hs.inter ht)) (hu.inter (hs.diff ht))]
+  congr
+  grind
+
+theorem restrict_union_add_inter (hs : MeasurableSet s) (ht : MeasurableSet t) :
+    v.restrict (s ∪ t) + v.restrict (s ∩ t) = v.restrict s + v.restrict t := by
+  rw [← v.restrict_inter_add_diff (hs.union ht) ht, union_inter_cancel_right, union_diff_right,
+    ← v.restrict_inter_add_diff hs ht, add_comm, ← add_assoc, add_right_comm]
+
+theorem restrict_union (h : Disjoint s t) (hs : MeasurableSet s) (ht : MeasurableSet t) :
+    v.restrict (s ∪ t) = v.restrict s + v.restrict t := by
+  simp [← v.restrict_union_add_inter hs ht, disjoint_iff_inter_eq_empty.mp h]
+
 end Partition
 
 section Sub
@@ -1045,7 +1104,7 @@ theorem trans {u : VectorMeasure α L} {v : VectorMeasure α M} {w : VectorMeasu
   fun _ hs => huv <| hvw hs
 
 theorem zero (v : VectorMeasure α N) : (0 : VectorMeasure α M) ≪ᵥ v :=
-  fun s _ => VectorMeasure.zero_apply s
+  fun s _ => zero_apply s
 
 theorem neg_left {M : Type*} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M]
     {v : VectorMeasure α M} {w : VectorMeasure α N} (h : v ≪ᵥ w) : -v ≪ᵥ w := by

Mathlib/MeasureTheory/VectorMeasure/Decomposition/JordanSub.lean

@@ -76,20 +76,19 @@ theorem sub_toSignedMeasure_eq_toSignedMeasure_sub :
     sub_apply_eq_zero_of_isHahnDecomposition hs
   have h₂' := toSignedMeasure_congr <| restrict_eq_zero.mpr <|
   sub_apply_eq_zero_of_isHahnDecomposition hsc
-  have partition₁ := VectorMeasure.restrict_add_restrict_compl (μ - ν).toSignedMeasure
+  have partition₁ := VectorMeasure.restrict_add_restrict_compl (v := (μ - ν).toSignedMeasure)
     hs.measurableSet
-  have partition₂ := VectorMeasure.restrict_add_restrict_compl (ν - μ).toSignedMeasure
+  have partition₂ := VectorMeasure.restrict_add_restrict_compl (v := (ν - μ).toSignedMeasure)
     hs.measurableSet
   rw [toSignedMeasure_restrict_eq_restrict_toSignedMeasure _ _ hs.measurableSet,
     toSignedMeasure_restrict_eq_restrict_toSignedMeasure _ _ hs.measurableSet.compl]
     at partition₁ partition₂
   rw [h₁', h₂] at partition₁
   rw [h₁, h₂'] at partition₂
   simp only [toSignedMeasure_zero, zero_add] at partition₁ partition₂
-  rw [← VectorMeasure.restrict_add_restrict_compl μ.toSignedMeasure hs.measurableSet,
-    ← VectorMeasure.restrict_add_restrict_compl ν.toSignedMeasure hs.measurableSet,
+  rw [← VectorMeasure.restrict_add_restrict_compl (v := μ.toSignedMeasure) hs.measurableSet,
+    ← VectorMeasure.restrict_add_restrict_compl (v := ν.toSignedMeasure) hs.measurableSet,
     ← partition₁, ← partition₂]
-  repeat rw [sub_eq_add_neg]
   abel
 
 /-- The Jordan decomposition associated to the pair of mutually singular measures `μ - ν`

Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean

@@ -5,6 +5,8 @@ Authors: Oliver Butterley, Yoh Tanimoto
 -/
 module
 
+public import Mathlib.Analysis.Normed.Module.Basic
+public import Mathlib.MeasureTheory.Measure.Dirac
 public import Mathlib.MeasureTheory.VectorMeasure.Variation.Defs
 
 /-!
@@ -30,7 +32,7 @@ such vector-valued measures.
 
 public section
 
-open Finset
+open Finset Set
 open scoped ENNReal
 
 namespace MeasureTheory.VectorMeasure
@@ -39,9 +41,9 @@ variable {X V : Type*} {mX : MeasurableSpace X}
 
 section Basic
 
-variable [TopologicalSpace V] [ENormedAddCommMonoid V] [T2Space V] {μ ν : VectorMeasure X V}
+variable [TopologicalSpace V] [ENormedAddCommMonoid V] [T2Space V]
+  {μ ν : VectorMeasure X V} {s : Set X}
 
-@[simp]
 lemma variation_apply (μ : VectorMeasure X V) (s : Set X) :
     μ.variation s = preVariation (‖μ ·‖ₑ) (isSigmaSubadditiveSetFun_enorm μ) (by simp) s := rfl
 
@@ -96,14 +98,15 @@ lemma absolutelyContinuous (μ : VectorMeasure X V) : μ ≪ᵥ μ.ennrealVariat
     grw [enorm_measure_le_variation, ← ennrealVariation_apply _ hsm, hs]
   · exact μ.not_measurable' hsm
 
-lemma variation_le_of_forall_enorm_le {m : Measure X} (h : ∀ E, MeasurableSet E → ‖μ E‖ₑ ≤ m E) :
-    μ.variation ≤ m := by
-  refine Measure.le_intro fun s hs _ => ?_
+lemma variation_apply_le_of_forall_enorm_le {m : Measure X} (hs : MeasurableSet s)
+    (h : ∀ E, MeasurableSet E → E ⊆ s → ‖μ E‖ₑ ≤ m E) :
+    μ.variation s ≤ m s := by
   simp only [variation_apply, preVariation, ennrealToMeasure_apply hs, ennrealPreVariation_apply,
     preVariationFun, hs, dite_true, iSup_le_iff]
   intro i
   calc
-    ∑ x ∈ i.parts, ‖μ x‖ₑ ≤ ∑ x ∈ i.parts, m x := Finset.sum_le_sum (fun s hs => h s s.property)
+    ∑ x ∈ i.parts, ‖μ x‖ₑ ≤ ∑ x ∈ i.parts, m x := Finset.sum_le_sum
+        (fun s hs => h s s.property (i.le hs))
     _ = m (i.parts.sup Subtype.val) := by
       rw [sup_set_eq_biUnion]
       refine (MeasureTheory.measure_biUnion_finset ?_ fun b _ => b.property).symm
@@ -113,6 +116,10 @@ lemma variation_le_of_forall_enorm_le {m : Measure X} (h : ∀ E, MeasurableSet
       rw [sup_set_eq_biUnion]
       exact measure_mono <| Set.iUnion₂_subset fun _ hp => Subtype.coe_le_coe.mpr (i.le hp)
 
+lemma variation_le_of_forall_enorm_le {m : Measure X} (h : ∀ E, MeasurableSet E → ‖μ E‖ₑ ≤ m E) :
+    μ.variation ≤ m :=
+  Measure.le_intro fun _ hs _ => variation_apply_le_of_forall_enorm_le hs (fun E hE _ ↦ h E hE)
+
 lemma variation_add_le [ContinuousAdd V] : variation (μ + ν) ≤ variation μ + variation ν := by
   refine variation_le_of_forall_enorm_le fun E _ => ?_
   calc
@@ -129,6 +136,90 @@ lemma variation_finsetSum_le [ContinuousAdd V] {ι} (s : Finset ι) (μ : ι →
     simpa [Finset.sum_insert his] using
       variation_add_le.trans (add_le_add_right ih ((μ i).variation))
 
+lemma variation_apply_eq_zero (hs : MeasurableSet s) :
+    μ.variation s = 0 ↔ ∀ t, t ⊆ s → MeasurableSet t → μ t = 0 := by
+  refine ⟨fun h t hts ht ↦ ?_, fun h ↦ ?_⟩
+  · rw [← enorm_eq_zero, ← le_zero_iff, ← h]
+    apply (enorm_measure_le_variation _ _).trans (measure_mono hts)
+  · suffices μ.variation s ≤ (0 : Measure X) s by simpa
+    apply variation_apply_le_of_forall_enorm_le hs (fun t ht hts ↦ ?_)
+    simp [h t hts ht]
+
+@[simp] lemma variation_eq_zero :
+    μ.variation = 0 ↔ μ = 0 where
+  mp h := by
+    ext s hs
+    apply enorm_eq_zero.1
+    apply le_antisymm ?_ (by simp)
+    grw [enorm_measure_le_variation]
+    simp [h]
+  mpr h := by simp [h]
+
+lemma variation_restrict (hs : MeasurableSet s) :
+    (μ.restrict s).variation = μ.variation.restrict s := by
+  apply le_antisymm
+  · apply variation_le_of_forall_enorm_le (fun t ht ↦ ?_)
+    simp only [ht, Measure.restrict_apply, VectorMeasure.restrict_apply, hs]
+    apply enorm_measure_le_variation
+  · apply Measure.le_iff.2 (fun t ht ↦ ?_)
+    simp only [ht, Measure.restrict_apply]
+    calc μ.variation (t ∩ s)
+    _ ≤ (μ.restrict s).variation (t ∩ s) := by
+      apply variation_apply_le_of_forall_enorm_le (ht.inter hs) (fun u u_meas hu ↦ ?_)
+      have : μ u = μ.restrict s u :=
+        (VectorMeasure.restrict_eq_self _ hs u_meas (hu.trans inter_subset_right)).symm
+      rw [this]
+      apply enorm_measure_le_variation
+    _ ≤ (μ.restrict s).variation t := by
+      gcongr
+      exact Set.inter_subset_left
+
+lemma variation_restrict_le : (μ.restrict s).variation ≤ μ.variation.restrict s := by
+  by_cases hs : MeasurableSet s
+  · simp [variation_restrict hs]
+  · simp [restrict_not_measurable _ hs, Measure.zero_le]
+
+instance [IsFiniteMeasure μ.variation] : IsFiniteMeasure (μ.restrict s).variation :=
+  isFiniteMeasure_of_le _ variation_restrict_le
+
+variable {Y : Type*} [MeasurableSpace Y] {φ : X → Y}
+
+lemma variation_map_le : (μ.map φ).variation ≤ μ.variation.map φ := by
+  by_cases hφ : Measurable φ; swap
+  · simp [VectorMeasure.map, hφ, Measure.zero_le]
+  apply variation_le_of_forall_enorm_le (fun s hs ↦ ?_)
+  simp [VectorMeasure.map_apply _ hφ hs, Measure.map_apply hφ hs, enorm_measure_le_variation]
+
+instance [IsFiniteMeasure μ.variation] : IsFiniteMeasure (μ.map φ).variation :=
+  isFiniteMeasure_of_le _ variation_map_le
+
+theorem _root_.MeasurableEmbedding.variation_map (hφ : MeasurableEmbedding φ) :
+    (μ.map φ).variation = μ.variation.map φ := by
+  apply le_antisymm variation_map_le ?_
+  apply Measure.le_iff.2 (fun s hs ↦ ?_)
+  simp only [hφ.measurable, hs, Measure.map_apply]
+  have : (μ.map φ).variation s = (μ.map φ).variation (s ∩ range φ) := by
+    nth_rw 1 [← inter_union_diff s (range φ)]
+    have : (μ.map φ).variation (s \ range φ) = 0 := by
+      apply (variation_apply_eq_zero (hs.diff hφ.measurableSet_range)).2 (fun t ht t_meas ↦ ?_)
+      have : φ ⁻¹' t = ∅ := by grind
+      simp [map_apply, t_meas, hφ.measurable, this]
+    rw [measure_union (by grind) (hs.diff hφ.measurableSet_range), this, add_zero]
+  rw [this, ← hφ.comap_preimage]
+  apply variation_le_of_forall_enorm_le (fun t ht ↦ ?_)
+  simp only [hφ.comap_apply]
+  apply le_trans ?_ (enorm_measure_le_variation _ _)
+  rw [map_apply _ hφ.measurable (hφ.measurableSet_image.2 ht), preimage_image_eq _ hφ.injective]
+
+@[simp] lemma variation_dirac {x : X} {v : V} :
+    (VectorMeasure.dirac x v).variation = ‖v‖ₑ • Measure.dirac x := by
+  apply le_antisymm
+  · apply variation_le_of_forall_enorm_le (fun s hs ↦ ?_)
+    by_cases hx : x ∈ s <;> simp [hs, hx]
+  · apply Measure.le_iff.2 (fun s hs ↦ ?_)
+    apply le_trans ?_ (enorm_measure_le_variation _ _)
+    by_cases hx : x ∈ s <;> simp [hs, hx]
+
 end Basic
 
 section NormedAddCommGroup
@@ -147,6 +238,42 @@ lemma variation_neg : (-μ).variation = μ.variation := by simp [variation]
 lemma variation_sub_le : (μ - ν).variation ≤ μ.variation + ν.variation := by
   grw [sub_eq_add_neg, variation_add_le, variation_neg]
 
+private lemma variation_smul_le {𝕜 : Type*} [NormedField 𝕜] [NormedSpace 𝕜 V] {c : 𝕜} :
+    (c • μ).variation ≤ ‖c‖₊ • μ.variation := by
+  apply variation_le_of_forall_enorm_le (fun s hs ↦ ?_)
+  simp only [coe_smul, Pi.smul_apply, enorm_smul, Measure.smul_apply, Measure.nnreal_smul_coe_apply]
+  grw [enorm_measure_le_variation, enorm_eq_nnnorm]
+
+lemma variation_smul {𝕜 : Type*} [NormedField 𝕜] [NormedSpace 𝕜 V] {c : 𝕜} :
+    (c • μ).variation = ‖c‖₊ • μ.variation := by
+  apply le_antisymm variation_smul_le ?_
+  rcases eq_or_ne c 0 with rfl | hc
+  · simp
+  calc ‖c‖₊ • μ.variation
+  _ = ‖c‖₊ • (c⁻¹ • (c • μ)).variation := by simp [smul_smul, inv_mul_cancel₀ hc]
+  _ ≤ ‖c‖₊ • ‖c⁻¹‖₊ • (c • μ).variation := by
+    gcongr
+    exact variation_smul_le
+  _ = (c • μ).variation := by
+    simp [smul_smul, mul_inv_cancel₀ (nnnorm_ne_zero_iff.mpr hc)]
+
+instance {𝕜 : Type*} [NormedField 𝕜] [NormedSpace 𝕜 V] {c : 𝕜} [IsFiniteMeasure μ.variation] :
+    IsFiniteMeasure (c • μ).variation := by
+  simp only [variation_smul]
+  infer_instance
+
+instance [Finite X] : IsFiniteMeasure μ.variation where
+  measure_univ_lt_top := by
+    classical
+    let : Fintype X := Fintype.ofFinite X
+    simp only [variation_apply, preVariation_apply, MeasurableSet.univ, ennrealToMeasure_apply,
+      ennrealPreVariation_apply, preVariationFun, ↓reduceDIte, ← sup_univ_eq_ciSup]
+    exact (Finset.sup_lt_iff (by simp)).2 (fun b hb ↦ by simp [ENNReal.sum_lt_top, enorm_lt_top])
+
+instance {x : X} {v : V} : IsFiniteMeasure (VectorMeasure.dirac x v).variation := by
+  simp only [variation_dirac, enorm_eq_nnnorm, Measure.coe_nnreal_smul]
+  infer_instance
+
 end NormedAddCommGroup
 
 end MeasureTheory.VectorMeasure