feat(measure_theory/function/lp_space): generalize some integrable …

…lemmas to `mem_ℒp` (#11231)

I would like to define integrable as `mem_ℒp` for `p = 1` and remove the `has_finite_integral` prop. But first we need to generalize everything we have about `integrable` to `mem_ℒp`. This is one step towards that goal.

src/measure_theory/function/ess_sup.lean

@@ -3,7 +3,7 @@ Copyright (c) 2021 Rémy Degenne. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne
 -/
-import measure_theory.measure.measure_space
+import measure_theory.constructions.borel_space
 import order.filter.ennreal
 
 /-!
@@ -26,7 +26,7 @@ sense). We do not define that quantity here, which is simply the supremum of a m
 * `ess_inf f μ := μ.ae.liminf f`
 -/
 
-open measure_theory filter
+open measure_theory filter topological_space
 open_locale ennreal measure_theory
 
 variables {α β : Type*} {m : measurable_space α} {μ ν : measure α}
@@ -128,6 +128,58 @@ begin
   simp [hc],
 end
 
+section topological_space
+
+variables {γ : Type*} {mγ : measurable_space γ} {f : α → γ} {g : γ → β}
+
+include mγ
+
+lemma ess_sup_comp_le_ess_sup_map_measure (hf : measurable f) :
+  ess_sup (g ∘ f) μ ≤ ess_sup g (measure.map f μ) :=
+begin
+  refine Limsup_le_Limsup_of_le (λ t, _) (by is_bounded_default) (by is_bounded_default),
+  simp_rw filter.mem_map,
+  have : (g ∘ f) ⁻¹' t = f ⁻¹' (g ⁻¹' t), by { ext1 x, simp_rw set.mem_preimage, },
+  rw this,
+  exact λ h, mem_ae_of_mem_ae_map hf h,
+end
+
+lemma _root_.measurable_embedding.ess_sup_map_measure (hf : measurable_embedding f) :
+  ess_sup g (measure.map f μ) = ess_sup (g ∘ f) μ :=
+begin
+  refine le_antisymm _ (ess_sup_comp_le_ess_sup_map_measure hf.measurable),
+  refine Limsup_le_Limsup (by is_bounded_default) (by is_bounded_default) (λ c h_le, _),
+  rw eventually_map at h_le ⊢,
+  exact hf.ae_map_iff.mpr h_le,
+end
+
+variables [measurable_space β] [topological_space β] [second_countable_topology β]
+  [order_closed_topology β] [opens_measurable_space β]
+
+lemma ess_sup_map_measure_of_measurable (hg : measurable g) (hf : measurable f) :
+  ess_sup g (measure.map f μ) = ess_sup (g ∘ f) μ :=
+begin
+  refine le_antisymm _ (ess_sup_comp_le_ess_sup_map_measure hf),
+  refine Limsup_le_Limsup (by is_bounded_default) (by is_bounded_default) (λ c h_le, _),
+  rw eventually_map at h_le ⊢,
+  rw ae_map_iff hf (measurable_set_le hg measurable_const),
+  exact h_le,
+end
+
+lemma ess_sup_map_measure (hg : ae_measurable g (measure.map f μ)) (hf : measurable f) :
+  ess_sup g (measure.map f μ) = ess_sup (g ∘ f) μ :=
+begin
+  rw [ess_sup_congr_ae hg.ae_eq_mk, ess_sup_map_measure_of_measurable hg.measurable_mk hf],
+  refine ess_sup_congr_ae _,
+  have h_eq := ae_of_ae_map hf hg.ae_eq_mk,
+  rw ← eventually_eq at h_eq,
+  exact h_eq.symm,
+end
+
+omit mγ
+
+end topological_space
+
 end complete_lattice
 
 section complete_linear_order

src/measure_theory/function/l1_space.lean

@@ -443,14 +443,18 @@ by { rw ← mem_ℒp_one_iff_integrable at hf ⊢, exact hf.of_measure_le_smul c
 
 lemma integrable.add_measure {f : α → β} (hμ : integrable f μ) (hν : integrable f ν) :
   integrable f (μ + ν) :=
-⟨hμ.ae_measurable.add_measure hν.ae_measurable,
-  hμ.has_finite_integral.add_measure hν.has_finite_integral⟩
+begin
+  simp_rw ← mem_ℒp_one_iff_integrable at hμ hν ⊢,
+  refine ⟨hμ.ae_measurable.add_measure hν.ae_measurable, _⟩,
+  rw [snorm_one_add_measure, ennreal.add_lt_top],
+  exact ⟨hμ.snorm_lt_top, hν.snorm_lt_top⟩,
+end
 
 lemma integrable.left_of_add_measure {f : α → β} (h : integrable f (μ + ν)) : integrable f μ :=
-h.mono_measure $ measure.le_add_right $ le_rfl
+by { rw ← mem_ℒp_one_iff_integrable at h ⊢, exact h.left_of_add_measure, }
 
 lemma integrable.right_of_add_measure {f : α → β} (h : integrable f (μ + ν)) : integrable f ν :=
-h.mono_measure $ measure.le_add_left $ le_rfl
+by { rw ← mem_ℒp_one_iff_integrable at h ⊢, exact h.right_of_add_measure, }
 
 @[simp] lemma integrable_add_measure {f : α → β} :
   integrable f (μ + ν) ↔ integrable f μ ∧ integrable f ν :=
@@ -467,21 +471,21 @@ by induction s using finset.induction_on; simp [*]
 
 lemma integrable.smul_measure {f : α → β} (h : integrable f μ) {c : ℝ≥0∞} (hc : c ≠ ∞) :
   integrable f (c • μ) :=
-⟨h.ae_measurable.smul_measure c, h.has_finite_integral.smul_measure hc⟩
+by { rw ← mem_ℒp_one_iff_integrable at h ⊢, exact h.smul_measure hc, }
 
 lemma integrable_map_measure [opens_measurable_space β] {f : α → δ} {g : δ → β}
   (hg : ae_measurable g (measure.map f μ)) (hf : measurable f) :
   integrable g (measure.map f μ) ↔ integrable (g ∘ f) μ :=
-by simp [integrable, hg, hg.comp_measurable hf, has_finite_integral, lintegral_map' hg.ennnorm hf]
+by { simp_rw ← mem_ℒp_one_iff_integrable, exact mem_ℒp_map_measure_iff hg hf, }
 
 lemma _root_.measurable_embedding.integrable_map_iff {f : α → δ} (hf : measurable_embedding f)
   {g : δ → β} :
   integrable g (measure.map f μ) ↔ integrable (g ∘ f) μ :=
-by simp only [integrable, hf.ae_measurable_map_iff, has_finite_integral, hf.lintegral_map]
+by { simp_rw ← mem_ℒp_one_iff_integrable, exact hf.mem_ℒp_map_measure_iff, }
 
 lemma integrable_map_equiv (f : α ≃ᵐ δ) (g : δ → β) :
   integrable g (measure.map f μ) ↔ integrable (g ∘ f) μ :=
-f.measurable_embedding.integrable_map_iff
+by { simp_rw ← mem_ℒp_one_iff_integrable, exact f.mem_ℒp_map_measure_iff, }
 
 lemma measure_preserving.integrable_comp [opens_measurable_space β] {ν : measure δ} {g : δ → β}
   {f : α → δ} (hf : measure_preserving f μ ν) (hg : ae_measurable g ν) :

src/measure_theory/function/lp_space.lean

@@ -601,6 +601,32 @@ begin
   simp [hc, hc0],
 end
 
+lemma mem_ℒp.smul_measure {f : α → E} {c : ℝ≥0∞} (hf : mem_ℒp f p μ) (hc : c ≠ ∞) :
+  mem_ℒp f p (c • μ) :=
+hf.of_measure_le_smul c hc le_rfl
+
+include m
+
+lemma snorm_one_add_measure (f : α → F) (μ ν : measure α) :
+  snorm f 1 (μ + ν) = snorm f 1 μ + snorm f 1 ν :=
+by { simp_rw snorm_one_eq_lintegral_nnnorm, rw lintegral_add_measure _ μ ν, }
+
+lemma snorm_le_add_measure_right (f : α → F) (μ ν : measure α) {p : ℝ≥0∞} :
+  snorm f p μ ≤ snorm f p (μ + ν) :=
+snorm_mono_measure f $ measure.le_add_right $ le_refl _
+
+lemma snorm_le_add_measure_left (f : α → F) (μ ν : measure α) {p : ℝ≥0∞} :
+  snorm f p ν ≤ snorm f p (μ + ν) :=
+snorm_mono_measure f $ measure.le_add_left $ le_refl _
+
+omit m
+
+lemma mem_ℒp.left_of_add_measure {f : α → E} (h : mem_ℒp f p (μ + ν)) : mem_ℒp f p μ :=
+h.mono_measure $ measure.le_add_right $ le_refl _
+
+lemma mem_ℒp.right_of_add_measure {f : α → E} (h : mem_ℒp f p (μ + ν)) : mem_ℒp f p ν :=
+h.mono_measure $ measure.le_add_left $ le_refl _
+
 section opens_measurable_space
 variable [opens_measurable_space E]
 
@@ -752,6 +778,63 @@ begin
   exact snorm'_add_lt_top_of_le_one hf.1 hg.1 hf.2 hg.2 hp_pos hp1_real,
 end
 
+section map_measure
+
+variables {β : Type*} {mβ : measurable_space β} {f : α → β} {g : β → E}
+
+include mβ
+
+lemma snorm_ess_sup_map_measure (hg : ae_measurable g (measure.map f μ)) (hf : measurable f) :
+  snorm_ess_sup g (measure.map f μ) = snorm_ess_sup (g ∘ f) μ :=
+ess_sup_map_measure hg.ennnorm hf
+
+lemma snorm_map_measure (hg : ae_measurable g (measure.map f μ)) (hf : measurable f) :
+  snorm g p (measure.map f μ) = snorm (g ∘ f) p μ :=
+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_map_measure hg hf, },
+  simp_rw snorm_eq_lintegral_rpow_nnnorm hp_zero hp_top,
+  rw lintegral_map' (hg.ennnorm.pow_const p.to_real) hf,
+end
+
+lemma mem_ℒp_map_measure_iff (hg : ae_measurable g (measure.map f μ)) (hf : measurable f) :
+  mem_ℒp g p (measure.map f μ) ↔ mem_ℒp (g ∘ f) p μ :=
+by simp [mem_ℒp, snorm_map_measure hg hf, hg.comp_measurable hf, hg]
+
+lemma _root_.measurable_embedding.snorm_ess_sup_map_measure {g : β → F}
+  (hf : measurable_embedding f) :
+  snorm_ess_sup g (measure.map f μ) = snorm_ess_sup (g ∘ f) μ :=
+hf.ess_sup_map_measure
+
+lemma _root_.measurable_embedding.snorm_map_measure {g : β → F} (hf : measurable_embedding f) :
+  snorm g p (measure.map f μ) = snorm (g ∘ f) p μ :=
+begin
+  by_cases hp_zero : p = 0,
+  { simp only [hp_zero, snorm_exponent_zero], },
+  by_cases hp : p = ∞,
+  { simp_rw [hp, snorm_exponent_top],
+    exact hf.ess_sup_map_measure, },
+  { simp_rw snorm_eq_lintegral_rpow_nnnorm hp_zero hp,
+    rw hf.lintegral_map, },
+end
+
+lemma _root_.measurable_embedding.mem_ℒp_map_measure_iff [measurable_space F] {g : β → F}
+  (hf : measurable_embedding f) :
+  mem_ℒp g p (measure.map f μ) ↔ mem_ℒp (g ∘ f) p μ :=
+by simp_rw [mem_ℒp, hf.ae_measurable_map_iff, hf.snorm_map_measure]
+
+lemma _root_.measurable_equiv.mem_ℒp_map_measure_iff [measurable_space F] (f : α ≃ᵐ β)
+  {g : β → F} :
+  mem_ℒp g p (measure.map f μ) ↔ mem_ℒp (g ∘ f) p μ :=
+f.measurable_embedding.mem_ℒp_map_measure_iff
+
+omit mβ
+
+end map_measure
+
 section trim
 
 lemma snorm'_trim (hm : m ≤ m0) {f : α → E} (hf : @measurable _ _ m _ f) :