diff --git a/Mathlib/Data/ENNReal/Action.lean b/Mathlib/Data/ENNReal/Action.lean index d6ba39d13c1c4c..431d6397d5b04d 100644 --- a/Mathlib/Data/ENNReal/Action.lean +++ b/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 diff --git a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean index dfdbb0f4299ba0..61ace844bbb268 100644 --- a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean +++ b/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 diff --git a/Mathlib/MeasureTheory/VectorMeasure/Basic.lean b/Mathlib/MeasureTheory/VectorMeasure/Basic.lean index e45965e0dbc9f6..84d98573283ec5 100644 --- a/Mathlib/MeasureTheory/VectorMeasure/Basic.lean +++ b/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,17 +635,22 @@ 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 @@ -649,7 +658,7 @@ 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 diff --git a/Mathlib/MeasureTheory/VectorMeasure/Decomposition/JordanSub.lean b/Mathlib/MeasureTheory/VectorMeasure/Decomposition/JordanSub.lean index 1ab015aac88725..026c666ed2b7ca 100644 --- a/Mathlib/MeasureTheory/VectorMeasure/Decomposition/JordanSub.lean +++ b/Mathlib/MeasureTheory/VectorMeasure/Decomposition/JordanSub.lean @@ -76,9 +76,9 @@ 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] @@ -86,10 +86,9 @@ theorem sub_toSignedMeasure_eq_toSignedMeasure_sub : 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 `μ - ν` diff --git a/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean b/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean index 3722e32704c756..1abcebc11dcbbe 100644 --- a/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean +++ b/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