feat(measure_theory/vector_measure): a signed measure restricted on a…

… positive set is a unsigned measure (#8597)

This PR defines `signed_measure.to_measure` which is the measure corresponding to a signed measure restricted on some positive set. This definition is useful for the Jordan decomposition theorem.

src/measure_theory/measure/vector_measure.lean

@@ -676,6 +676,39 @@ begin
   rw [restrict_empty, restrict_empty]
 end
 
+lemma le_restrict_univ_iff_le : v ≤[univ] w ↔ v ≤ w :=
+begin
+  split,
+  { intros h s hs,
+    have := h s hs,
+    rwa [restrict_apply _ measurable_set.univ hs, inter_univ,
+         restrict_apply _ measurable_set.univ hs, inter_univ] at this },
+  { intros h s hs,
+    rw [restrict_apply _ measurable_set.univ hs, inter_univ,
+        restrict_apply _ measurable_set.univ hs, inter_univ],
+    exact h s hs }
+end
+
+end
+
+section
+
+variables {M : Type*} [topological_space M] [ordered_add_comm_group M] [topological_add_group M]
+variables (v w : vector_measure α M)
+
+lemma neg_le_neg {i : set α} (hi : measurable_set i) (h : v ≤[i] w) : -w ≤[i] -v :=
+begin
+  intros j hj₁,
+  rw [restrict_apply _ hi hj₁, restrict_apply _ hi hj₁, neg_apply, neg_apply],
+  refine neg_le_neg _,
+  rw [← restrict_apply _ hi hj₁, ← restrict_apply _ hi hj₁],
+  exact h j hj₁,
+end
+
+@[simp]
+lemma neg_le_neg_iff {i : set α} (hi : measurable_set i) : -w ≤[i] -v ↔ v ≤[i] w :=
+⟨λ h, neg_neg v ▸ neg_neg w ▸ neg_le_neg _ _ hi h, λ h, neg_le_neg _ _ hi h⟩
+
 end
 
 section
@@ -815,4 +848,128 @@ end
 
 end vector_measure
 
+namespace signed_measure
+
+open vector_measure
+
+open_locale measure_theory
+
+/-- The underlying function for `signed_measure.to_measure_of_zero_le`. -/
+def to_measure_of_zero_le' (s : signed_measure α) (i : set α) (hi : 0 ≤[i] s)
+  (j : set α) (hj : measurable_set j) : ℝ≥0∞ :=
+@coe ℝ≥0 ℝ≥0∞ _ ⟨s.restrict i j, le_trans (by simp) (hi j hj)⟩
+
+/-- Given a signed measure `s` and a positive measurable set `i`, `to_measure_of_zero_le`
+provides the measure, mapping measurable sets `j` to `s (i ∩ j)`. -/
+def to_measure_of_zero_le (s : signed_measure α) (i : set α)
+  (hi₁ : measurable_set i) (hi₂ : 0 ≤[i] s) : measure α :=
+measure.of_measurable (s.to_measure_of_zero_le' i hi₂)
+  (by { simp_rw [to_measure_of_zero_le', s.restrict_apply hi₁ measurable_set.empty,
+                 set.empty_inter i, s.empty], refl })
+  begin
+    intros f hf₁ hf₂,
+    have h₁ : ∀ n, measurable_set (i ∩ f n) := λ n, hi₁.inter (hf₁ n),
+    have h₂ : pairwise (disjoint on λ (n : ℕ), i ∩ f n),
+    { rintro n m hnm x ⟨⟨_, hx₁⟩, _, hx₂⟩,
+      exact hf₂ n m hnm ⟨hx₁, hx₂⟩ },
+    simp only [to_measure_of_zero_le', s.restrict_apply hi₁ (measurable_set.Union hf₁),
+               set.inter_comm, set.inter_Union, s.of_disjoint_Union_nat h₁ h₂,
+               ennreal.some_eq_coe, id.def],
+    have h : ∀ n, 0 ≤ s (i ∩ f n) :=
+      λ n, s.nonneg_of_zero_le_restrict
+          (s.zero_le_restrict_subset hi₁ (inter_subset_left _ _) hi₂),
+    rw [nnreal.coe_tsum_of_nonneg h, ennreal.coe_tsum],
+    { refine tsum_congr (λ n, _),
+      simp_rw [s.restrict_apply hi₁ (hf₁ n), set.inter_comm] },
+    { exact (nnreal.summable_coe_of_nonneg h).2 (s.m_Union h₁ h₂).summable }
+  end
+
+variables (s : signed_measure α) {i j : set α}
+
+lemma to_measure_of_zero_le_apply (hi : 0 ≤[i] s)
+  (hi₁ : measurable_set i) (hj₁ : measurable_set j) :
+  s.to_measure_of_zero_le i hi₁ hi j =
+  @coe ℝ≥0 ℝ≥0∞ _ ⟨s (i ∩ j), nonneg_of_zero_le_restrict s
+    (zero_le_restrict_subset s hi₁ (set.inter_subset_left _ _) hi)⟩ :=
+by simp_rw [to_measure_of_zero_le, measure.of_measurable_apply _ hj₁, to_measure_of_zero_le',
+              s.restrict_apply hi₁ hj₁, set.inter_comm]
+
+/-- Given a signed measure `s` and a negative measurable set `i`, `to_measure_of_le_zero`
+provides the measure, mapping measurable sets `j` to `-s (i ∩ j)`. -/
+def to_measure_of_le_zero (s : signed_measure α) (i : set α) (hi₁ : measurable_set i)
+  (hi₂ : s ≤[i] 0) : measure α :=
+to_measure_of_zero_le (-s) i hi₁ $ (@neg_zero (vector_measure α ℝ) _) ▸ neg_le_neg _ _ hi₁ hi₂
+
+lemma to_measure_of_le_zero_apply (hi : s ≤[i] 0)
+  (hi₁ : measurable_set i) (hj₁ : measurable_set j) :
+  s.to_measure_of_le_zero i hi₁ hi j =
+  @coe ℝ≥0 ℝ≥0∞ _ ⟨-s (i ∩ j), neg_apply s (i ∩ j) ▸ nonneg_of_zero_le_restrict _
+    (zero_le_restrict_subset _ hi₁ (set.inter_subset_left _ _)
+    ((@neg_zero (vector_measure α ℝ) _) ▸ neg_le_neg _ _ hi₁ hi))⟩ :=
+begin
+  erw [to_measure_of_zero_le_apply],
+  { simp },
+  { assumption },
+end
+
+/-- `signed_measure.to_measure_of_zero_le` is a finite measure. -/
+instance to_measure_of_zero_le_finite (hi : 0 ≤[i] s) (hi₁ : measurable_set i) :
+  finite_measure (s.to_measure_of_zero_le i hi₁ hi) :=
+{ measure_univ_lt_top :=
+  begin
+    rw [to_measure_of_zero_le_apply s hi hi₁ measurable_set.univ],
+    exact ennreal.coe_lt_top,
+  end }
+
+/-- `signed_measure.to_measure_of_le_zero` is a finite measure. -/
+instance to_measure_of_le_zero_finite (hi : s ≤[i] 0) (hi₁ : measurable_set i) :
+  finite_measure (s.to_measure_of_le_zero i hi₁ hi) :=
+{ measure_univ_lt_top :=
+  begin
+    rw [to_measure_of_le_zero_apply s hi hi₁ measurable_set.univ],
+    exact ennreal.coe_lt_top,
+  end }
+
+lemma to_measure_of_zero_le_to_signed_measure (hs : 0 ≤[univ] s) :
+  (s.to_measure_of_zero_le univ measurable_set.univ hs).to_signed_measure = s :=
+begin
+  ext i hi,
+  simp [measure.to_signed_measure_apply_measurable hi, to_measure_of_zero_le_apply _ _ _ hi],
+end
+
+lemma to_measure_of_le_zero_to_signed_measure (hs : s ≤[univ] 0) :
+  (s.to_measure_of_le_zero univ measurable_set.univ hs).to_signed_measure = -s :=
+begin
+  ext i hi,
+  simp [measure.to_signed_measure_apply_measurable hi, to_measure_of_le_zero_apply _ _ _ hi],
+end
+
+end signed_measure
+
+namespace measure
+
+open vector_measure
+
+variables (μ : measure α) [finite_measure μ]
+
+lemma zero_le_to_signed_measure : 0 ≤ μ.to_signed_measure :=
+begin
+  rw ← le_restrict_univ_iff_le,
+  refine restrict_le_restrict_of_subset_le _ _ (λ j hj₁ _, _),
+  simp only [measure.to_signed_measure_apply_measurable hj₁, coe_zero, pi.zero_apply,
+             ennreal.to_real_nonneg, vector_measure.coe_zero]
+end
+
+lemma to_signed_measure_to_measure_of_zero_le :
+  μ.to_signed_measure.to_measure_of_zero_le univ measurable_set.univ
+    ((le_restrict_univ_iff_le _ _).2 (zero_le_to_signed_measure μ)) = μ :=
+begin
+  refine measure.ext (λ i hi, _),
+  lift μ i to ℝ≥0 using (measure_lt_top _ _).ne with m hm,
+  simp [signed_measure.to_measure_of_zero_le_apply _ _ _ hi,
+        measure.to_signed_measure_apply_measurable hi, ← hm],
+end
+
+end measure
+
 end measure_theory

src/topology/instances/nnreal.lean

@@ -134,13 +134,27 @@ begin
   exact assume ⟨a, ha⟩, ⟨a.1, has_sum_coe.2 ha⟩
 end
 
+lemma summable_coe_of_nonneg {f : α → ℝ} (hf₁ : ∀ n, 0 ≤ f n) :
+  @summable (ℝ≥0) _ _ _ (λ n, ⟨f n, hf₁ n⟩) ↔ summable f :=
+begin
+  lift f to α → ℝ≥0 using hf₁ with f rfl hf₁,
+  simp only [summable_coe, subtype.coe_eta]
+end
+
 open_locale classical
 
 @[norm_cast] lemma coe_tsum {f : α → ℝ≥0} : ↑∑'a, f a = ∑'a, (f a : ℝ) :=
 if hf : summable f
 then (eq.symm $ (has_sum_coe.2 $ hf.has_sum).tsum_eq)
 else by simp [tsum, hf, mt summable_coe.1 hf]
 
+lemma coe_tsum_of_nonneg {f : α → ℝ} (hf₁ : ∀ n, 0 ≤ f n) :
+  (⟨∑' n, f n, tsum_nonneg hf₁⟩ : ℝ≥0) = (∑' n, ⟨f n, hf₁ n⟩ : ℝ≥0) :=
+begin
+  lift f to α → ℝ≥0 using hf₁ with f rfl hf₁,
+  simp_rw [← nnreal.coe_tsum, subtype.coe_eta]
+end
+
 lemma tsum_mul_left (a : ℝ≥0) (f : α → ℝ≥0) : ∑' x, a * f x = a * ∑' x, f x :=
 nnreal.eq $ by simp only [coe_tsum, nnreal.coe_mul, tsum_mul_left]