feat(measure_theory/function/lp_space): add mem_Lp_indicator_iff_rest…

…rict (#9221)

We have an equivalent lemma for `integrable`. Here it is generalized to `mem_ℒp`.

src/measure_theory/function/ess_sup.lean

@@ -139,6 +139,34 @@ 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
+  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,
+  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, _),
+  by_cases hxs : x ∈ s,
+  { simpa [hxs] using hxc hxs, },
+  { simpa [hxs] using hc, },
+end
+
 end complete_linear_order
 
 namespace ennreal

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 _ hμs,
-  exact (ennreal.rpow_lt_top_of_nonneg hp_pos.le ennreal.coe_ne_top).ne,
+  { 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

src/measure_theory/measure/measure_space.lean

@@ -1450,6 +1450,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]
 
@@ -2812,6 +2816,37 @@ 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,
+  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,
+  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⟩