From 7b27f461166b82a4d73ae70b9b9750cd0f16a204 Mon Sep 17 00:00:00 2001 From: Kexing Ying Date: Thu, 12 Aug 2021 16:55:31 +0000 Subject: [PATCH] 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. --- .../measure/vector_measure.lean | 157 ++++++++++++++++++ src/topology/instances/nnreal.lean | 14 ++ 2 files changed, 171 insertions(+) diff --git a/src/measure_theory/measure/vector_measure.lean b/src/measure_theory/measure/vector_measure.lean index b9d260e8f2be1..d822a2417c340 100644 --- a/src/measure_theory/measure/vector_measure.lean +++ b/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 diff --git a/src/topology/instances/nnreal.lean b/src/topology/instances/nnreal.lean index 27f38c343a2be..b15be55e4ea07 100644 --- a/src/topology/instances/nnreal.lean +++ b/src/topology/instances/nnreal.lean @@ -134,6 +134,13 @@ 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 : ℝ) := @@ -141,6 +148,13 @@ 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]