From 2360b1f2f96adbf2654f628efff78f2438e8c966 Mon Sep 17 00:00:00 2001 From: RemyDegenne Date: Wed, 15 Sep 2021 15:58:38 +0200 Subject: [PATCH 1/6] snorm_indicator --- src/measure_theory/function/ess_sup.lean | 31 +++++++++ src/measure_theory/function/lp_space.lean | 66 ++++++++++++++----- src/measure_theory/measure/measure_space.lean | 37 +++++++++++ 3 files changed, 116 insertions(+), 18 deletions(-) diff --git a/src/measure_theory/function/ess_sup.lean b/src/measure_theory/function/ess_sup.lean index fe03bb2765914..a4464f643fe43 100644 --- a/src/measure_theory/function/ess_sup.lean +++ b/src/measure_theory/function/ess_sup.lean @@ -139,6 +139,37 @@ filter.eventually_lt_of_limsup_lt hf lemma ae_lt_of_lt_ess_inf {f : α → β} {x : β} (hf : x < ess_inf f μ) : ∀ᵐ y ∂μ, x < f y := @ae_lt_of_ess_sup_lt α (order_dual β) _ _ _ _ _ hf +lemma ess_sup_indicator_eq_ess_sup_restrict [has_zero β] {s : set α} + {f : α → β} (hf : 0 ≤ᵐ[μ.restrict s] f) (hs : measurable_set s) (hs_not_null : μ s ≠ 0) : + ess_sup (s.indicator f) μ = ess_sup f (μ.restrict s) := +begin + simp_rw ess_sup, + refine le_antisymm _ _, + swap, { exact Limsup_le_Limsup_of_le (map_restrict_ae_le_map_indicator_ae hs) + (by is_bounded_default) (by is_bounded_default), }, + refine Limsup_le_Limsup (by is_bounded_default) (by is_bounded_default) (λ c h_restrict_le, _), + rw eventually_map at h_restrict_le ⊢, + rw ae_restrict_iff' hs at h_restrict_le, + have hc : 0 ≤ c, + { suffices : ∃ x, 0 ≤ f x ∧ f x ≤ c, by { obtain ⟨x, hx⟩ := this, exact hx.1.trans hx.2, }, + refine frequently.exists _, + { exact μ.ae, }, + rw [eventually_le, ae_restrict_iff' hs] at hf, + have hs' : ∃ᵐ x ∂μ, x ∈ s, + { contrapose! hs_not_null, + rw [not_frequently, ae_iff] at hs_not_null, + suffices : {a : α | ¬a ∉ s} = s, by rwa ← this, + simp, }, + refine hs'.mp (hf.mp (h_restrict_le.mono (λ x hxs_imp_c hxf_nonneg hxs, _))), + rw pi.zero_apply at hxf_nonneg, + exact ⟨hxf_nonneg hxs, hxs_imp_c hxs⟩, }, + refine h_restrict_le.mono (λ x hxc, _), + haveI : decidable (x ∈ s) := classical.dec _, + by_cases hxs : x ∈ s, + { simpa [hxs] using hxc hxs, }, + { simpa [hxs] using hc, }, +end + end complete_linear_order namespace ennreal diff --git a/src/measure_theory/function/lp_space.lean b/src/measure_theory/function/lp_space.lean index 1de1a9211e0c5..33d4a6efb86a3 100644 --- a/src/measure_theory/function/lp_space.lean +++ b/src/measure_theory/function/lp_space.lean @@ -1563,28 +1563,58 @@ lemma mem_ℒp.indicator (hs : measurable_set s) (hf : mem_ℒp f p μ) : mem_ℒp (s.indicator f) p μ := ⟨hf.ae_measurable.indicator hs, lt_of_le_of_lt (snorm_indicator_le f) hf.snorm_lt_top⟩ +lemma snorm_ess_sup_indicator_eq_snorm_ess_sup_restrict {f : α → F} (hs : measurable_set s) : + snorm_ess_sup (s.indicator f) μ = snorm_ess_sup f (μ.restrict s) := +begin + simp_rw [snorm_ess_sup, nnnorm_indicator_eq_indicator_nnnorm, ennreal.coe_indicator], + by_cases hs_null : μ s = 0, + { rw measure.restrict_zero_set hs_null, + simp only [ess_sup_measure_zero, ennreal.ess_sup_eq_zero_iff, ennreal.bot_eq_zero], + have hs_empty : s =ᵐ[μ] (∅ : set α), by { rw ae_eq_set, simpa using hs_null, }, + refine (indicator_ae_eq_of_ae_eq_set hs_empty).trans _, + rw set.indicator_empty, + refl, }, + rw ess_sup_indicator_eq_ess_sup_restrict (eventually_of_forall (λ x, _)) hs hs_null, + rw pi.zero_apply, + exact zero_le _, +end + +lemma snorm_indicator_eq_snorm_restrict {f : α → F} (hs : measurable_set s) : + snorm (s.indicator f) p μ = snorm f p (μ.restrict s) := +begin + by_cases hp_zero : p = 0, + { simp only [hp_zero, snorm_exponent_zero], }, + by_cases hp_top : p = ∞, + { simp_rw [hp_top, snorm_exponent_top], + exact snorm_ess_sup_indicator_eq_snorm_ess_sup_restrict hs, }, + simp_rw snorm_eq_lintegral_rpow_nnnorm hp_zero hp_top, + suffices : ∫⁻ x, ∥s.indicator f x∥₊ ^ p.to_real ∂μ = ∫⁻ x in s, ∥f x∥₊ ^ p.to_real ∂μ, + by rw this, + rw ← lintegral_indicator _ hs, + congr, + simp_rw [nnnorm_indicator_eq_indicator_nnnorm, ennreal.coe_indicator], + have h_zero : (λ x, x ^ p.to_real) (0 : ℝ≥0∞) = 0, + by simp [ennreal.to_real_pos_iff.mpr ⟨ne.bot_lt hp_zero, hp_top⟩], + exact (set.indicator_comp_of_zero h_zero).symm, +end + +lemma mem_ℒp_indicator_iff_restrict (hs : measurable_set s) : + mem_ℒp (s.indicator f) p μ ↔ mem_ℒp f p (μ.restrict s) := +by simp [mem_ℒp, ae_measurable_indicator_iff hs, snorm_indicator_eq_snorm_restrict hs] + lemma mem_ℒp_indicator_const (p : ℝ≥0∞) (hs : measurable_set s) (c : E) (hμsc : c = 0 ∨ μ s ≠ ∞) : mem_ℒp (s.indicator (λ _, c)) p μ := begin - cases hμsc with hc hμs, - { simp only [hc, set.indicator_zero], - exact zero_mem_ℒp, }, - refine ⟨(ae_measurable_indicator_iff hs).mpr ae_measurable_const, _⟩, - by_cases hp0 : p = 0, - { simp only [hp0, snorm_exponent_zero, with_top.zero_lt_top], }, + rw mem_ℒp_indicator_iff_restrict hs, + by_cases hp_zero : p = 0, + { rw hp_zero, exact mem_ℒp_zero_iff_ae_measurable.mpr ae_measurable_const, }, by_cases hp_top : p = ∞, - { rw [hp_top, snorm_exponent_top], - exact (snorm_ess_sup_indicator_const_le s c).trans_lt ennreal.coe_lt_top, }, - have hp_pos : 0 < p.to_real, - from ennreal.to_real_pos_iff.mpr ⟨lt_of_le_of_ne (zero_le _) (ne.symm hp0), hp_top⟩, - rw snorm_lt_top_iff_lintegral_rpow_nnnorm_lt_top hp0 hp_top, - simp_rw [nnnorm_indicator_eq_indicator_nnnorm, ennreal.coe_indicator], - have h_indicator_pow : (λ a : α, s.indicator (λ _, (∥c∥₊ : ℝ≥0∞)) a ^ p.to_real) - = s.indicator (λ _, ↑∥c∥₊ ^ p.to_real), - { rw set.comp_indicator_const (∥c∥₊ : ℝ≥0∞) (λ x, x ^ p.to_real) _, simp [hp_pos], }, - rw [h_indicator_pow, lintegral_indicator _ hs, set_lintegral_const], - refine ennreal.mul_lt_top _ (lt_top_iff_ne_top.mpr hμs), - exact ennreal.rpow_lt_top_of_nonneg hp_pos.le ennreal.coe_ne_top, + { rw hp_top, + exact mem_ℒp_top_of_bound ae_measurable_const (∥c∥) (eventually_of_forall (λ x, le_rfl)), }, + rw [mem_ℒp_const_iff hp_zero hp_top, measure.restrict_apply_univ], + cases hμsc, + { exact or.inl hμsc, }, + { exact or.inr hμsc.lt_top, }, end end indicator diff --git a/src/measure_theory/measure/measure_space.lean b/src/measure_theory/measure/measure_space.lean index e24b519649588..c0157dd6e3075 100644 --- a/src/measure_theory/measure/measure_space.lean +++ b/src/measure_theory/measure/measure_space.lean @@ -1438,6 +1438,10 @@ begin { exact hx1 hxt, }, end +lemma mem_map_restrict_ae_iff {β} {s : set α} {t : set β} {f : α → β} (hs : measurable_set s) : + t ∈ filter.map f (μ.restrict s).ae ↔ μ ((f ⁻¹' t)ᶜ ∩ s) = 0 := +by rw [mem_map, mem_ae_iff, measure.restrict_apply' hs] + lemma ae_smul_measure {p : α → Prop} (h : ∀ᵐ x ∂μ, p x) (c : ℝ≥0∞) : ∀ᵐ x ∂(c • μ), p x := ae_iff.2 $ by rw [smul_apply, ae_iff.1 h, mul_zero] @@ -2801,6 +2805,39 @@ section indicator_function variables [measurable_space α] {μ : measure α} {s t : set α} {f : α → β} +lemma mem_map_indicator_ae_iff_mem_map_restrict_ae_of_zero_mem [has_zero β] {t : set β} + (ht : (0 : β) ∈ t) (hs : measurable_set s) : + t ∈ filter.map (s.indicator f) μ.ae ↔ t ∈ filter.map f (μ.restrict s).ae := +begin + simp_rw [mem_map, mem_ae_iff], + rw [measure.restrict_apply' hs, set.indicator_preimage, set.ite], + simp_rw [set.compl_union, set.compl_inter], + change μ (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ ((λ x, (0 : β)) ⁻¹' t \ s)ᶜ) = 0 ↔ μ ((f ⁻¹' t)ᶜ ∩ s) = 0, + haveI : decidable ((0 : β) ∈ t), from classical.dec _, + simp only [ht, ← set.compl_eq_univ_diff, compl_compl, set.compl_union, if_true, + set.preimage_const], + simp_rw [set.union_inter_distrib_right, set.compl_inter_self s, set.union_empty], +end + +lemma mem_map_indicator_ae_iff_of_zero_nmem [has_zero β] {t : set β} (ht : (0 : β) ∉ t) : + t ∈ filter.map (s.indicator f) μ.ae ↔ μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 0 := +begin + rw [mem_map, mem_ae_iff, set.indicator_preimage, set.ite, set.compl_union, set.compl_inter], + change μ (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ ((λ x, (0 : β)) ⁻¹' t \ s)ᶜ) = 0 ↔ μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 0, + haveI : decidable ((0 : β) ∈ t), from classical.dec _, + simp only [ht, if_false, set.compl_empty, set.empty_diff, set.inter_univ, set.preimage_const], +end + +lemma map_restrict_ae_le_map_indicator_ae [has_zero β] (hs : measurable_set s) : + filter.map f (μ.restrict s).ae ≤ filter.map (s.indicator f) μ.ae := +begin + intro t, + by_cases ht : (0 : β) ∈ t, + { rw mem_map_indicator_ae_iff_mem_map_restrict_ae_of_zero_mem ht hs, exact id, }, + rw [mem_map_indicator_ae_iff_of_zero_nmem ht, mem_map_restrict_ae_iff hs], + exact λ h, measure_mono_null ((set.inter_subset_left _ _).trans (set.subset_union_left _ _)) h, +end + lemma ae_measurable.restrict [measurable_space β] (hfm : ae_measurable f μ) {s} : ae_measurable f (μ.restrict s) := ⟨ae_measurable.mk f hfm, hfm.measurable_mk, ae_restrict_of_ae hfm.ae_eq_mk⟩ From 0d746ad8e8d564ab0ec21b9c5b643fe743f36d91 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9my=20Degenne?= Date: Sat, 18 Sep 2021 17:26:08 +0200 Subject: [PATCH 2/6] Update src/measure_theory/function/ess_sup.lean Co-authored-by: sgouezel --- src/measure_theory/function/ess_sup.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/src/measure_theory/function/ess_sup.lean b/src/measure_theory/function/ess_sup.lean index a4464f643fe43..2316086eabe0c 100644 --- a/src/measure_theory/function/ess_sup.lean +++ b/src/measure_theory/function/ess_sup.lean @@ -143,7 +143,6 @@ lemma ess_sup_indicator_eq_ess_sup_restrict [has_zero β] {s : set α} {f : α → β} (hf : 0 ≤ᵐ[μ.restrict s] f) (hs : measurable_set s) (hs_not_null : μ s ≠ 0) : ess_sup (s.indicator f) μ = ess_sup f (μ.restrict s) := begin - simp_rw ess_sup, refine le_antisymm _ _, swap, { exact Limsup_le_Limsup_of_le (map_restrict_ae_le_map_indicator_ae hs) (by is_bounded_default) (by is_bounded_default), }, From 79ef5d2c34990b0b933ac7ffc29f6a3c0c9c6d40 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9my=20Degenne?= Date: Sat, 18 Sep 2021 17:26:15 +0200 Subject: [PATCH 3/6] Update src/measure_theory/function/ess_sup.lean Co-authored-by: sgouezel --- src/measure_theory/function/ess_sup.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/measure_theory/function/ess_sup.lean b/src/measure_theory/function/ess_sup.lean index 2316086eabe0c..30edcdfedaba6 100644 --- a/src/measure_theory/function/ess_sup.lean +++ b/src/measure_theory/function/ess_sup.lean @@ -143,9 +143,8 @@ lemma ess_sup_indicator_eq_ess_sup_restrict [has_zero β] {s : set α} {f : α → β} (hf : 0 ≤ᵐ[μ.restrict s] f) (hs : measurable_set s) (hs_not_null : μ s ≠ 0) : ess_sup (s.indicator f) μ = ess_sup f (μ.restrict s) := begin - refine le_antisymm _ _, - swap, { exact Limsup_le_Limsup_of_le (map_restrict_ae_le_map_indicator_ae hs) - (by is_bounded_default) (by is_bounded_default), }, + refine le_antisymm _ (Limsup_le_Limsup_of_le (map_restrict_ae_le_map_indicator_ae hs) + (by is_bounded_default) (by is_bounded_default)), refine Limsup_le_Limsup (by is_bounded_default) (by is_bounded_default) (λ c h_restrict_le, _), rw eventually_map at h_restrict_le ⊢, rw ae_restrict_iff' hs at h_restrict_le, From e4a0c889876e5b2e2227ecfeaff30c3c2f5b8ab2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9my=20Degenne?= Date: Sat, 18 Sep 2021 17:29:10 +0200 Subject: [PATCH 4/6] Update src/measure_theory/function/ess_sup.lean Co-authored-by: sgouezel --- src/measure_theory/function/ess_sup.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/src/measure_theory/function/ess_sup.lean b/src/measure_theory/function/ess_sup.lean index 30edcdfedaba6..c5715e937f7af 100644 --- a/src/measure_theory/function/ess_sup.lean +++ b/src/measure_theory/function/ess_sup.lean @@ -162,7 +162,6 @@ begin rw pi.zero_apply at hxf_nonneg, exact ⟨hxf_nonneg hxs, hxs_imp_c hxs⟩, }, refine h_restrict_le.mono (λ x hxc, _), - haveI : decidable (x ∈ s) := classical.dec _, by_cases hxs : x ∈ s, { simpa [hxs] using hxc hxs, }, { simpa [hxs] using hc, }, From 4f6c24bb93e402b704c4a70c600f21203906709f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9my=20Degenne?= Date: Sat, 18 Sep 2021 17:29:15 +0200 Subject: [PATCH 5/6] Update src/measure_theory/measure/measure_space.lean Co-authored-by: sgouezel --- src/measure_theory/measure/measure_space.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/src/measure_theory/measure/measure_space.lean b/src/measure_theory/measure/measure_space.lean index c0157dd6e3075..4f5fd5a108f64 100644 --- a/src/measure_theory/measure/measure_space.lean +++ b/src/measure_theory/measure/measure_space.lean @@ -2813,7 +2813,6 @@ begin rw [measure.restrict_apply' hs, set.indicator_preimage, set.ite], simp_rw [set.compl_union, set.compl_inter], change μ (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ ((λ x, (0 : β)) ⁻¹' t \ s)ᶜ) = 0 ↔ μ ((f ⁻¹' t)ᶜ ∩ s) = 0, - haveI : decidable ((0 : β) ∈ t), from classical.dec _, simp only [ht, ← set.compl_eq_univ_diff, compl_compl, set.compl_union, if_true, set.preimage_const], simp_rw [set.union_inter_distrib_right, set.compl_inter_self s, set.union_empty], From c52b0476c5e3dbfd32b930942d91b86b12d1665b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9my=20Degenne?= Date: Sat, 18 Sep 2021 17:29:20 +0200 Subject: [PATCH 6/6] Update src/measure_theory/measure/measure_space.lean Co-authored-by: sgouezel --- src/measure_theory/measure/measure_space.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/src/measure_theory/measure/measure_space.lean b/src/measure_theory/measure/measure_space.lean index 4f5fd5a108f64..55bdd473f8eb7 100644 --- a/src/measure_theory/measure/measure_space.lean +++ b/src/measure_theory/measure/measure_space.lean @@ -2823,7 +2823,6 @@ lemma mem_map_indicator_ae_iff_of_zero_nmem [has_zero β] {t : set β} (ht : (0 begin rw [mem_map, mem_ae_iff, set.indicator_preimage, set.ite, set.compl_union, set.compl_inter], change μ (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ ((λ x, (0 : β)) ⁻¹' t \ s)ᶜ) = 0 ↔ μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 0, - haveI : decidable ((0 : β) ∈ t), from classical.dec _, simp only [ht, if_false, set.compl_empty, set.empty_diff, set.inter_univ, set.preimage_const], end