feat(measure_theory/function/l1_space): add integrability lemmas for composition with to_real (#9199)

Author: kex-y

src/measure_theory/function/l1_space.lean

@@ -224,6 +224,21 @@ lemma has_finite_integral_norm_iff (f : α → β) :
   has_finite_integral (λa, ∥f a∥) μ ↔ has_finite_integral f μ :=
 has_finite_integral_congr' $ eventually_of_forall $ λ x, norm_norm (f x)
 
+lemma has_finite_integral_to_real_of_lintegral_ne_top
+  {f : α → ℝ≥0∞} (hf : ∫⁻ x, f x ∂μ ≠ ∞) :
+  has_finite_integral (λ x, (f x).to_real) μ :=
+begin
+  have : ∀ x, (∥(f x).to_real∥₊ : ℝ≥0∞) =
+    @coe ℝ≥0 ℝ≥0∞ _ (⟨(f x).to_real, ennreal.to_real_nonneg⟩ : ℝ≥0),
+  { intro x, rw real.nnnorm_of_nonneg },
+  simp_rw [has_finite_integral, this],
+  refine lt_of_le_of_lt (lintegral_mono (λ x, _)) (lt_top_iff_ne_top.2 hf),
+  by_cases hfx : f x = ∞,
+  { simp [hfx] },
+  { lift f x to ℝ≥0 using hfx with fx,
+    simp [← h] }
+end
+
 lemma is_finite_measure_with_density_of_real {f : α → ℝ} (hfi : has_finite_integral f μ) :
   is_finite_measure (μ.with_density (λ x, ennreal.of_real $ f x)) :=
 is_finite_measure_with_density $
@@ -373,6 +388,7 @@ lemma has_finite_integral.const_mul {f : α → ℝ} (h : has_finite_integral f
 lemma has_finite_integral.mul_const {f : α → ℝ} (h : has_finite_integral f μ) (c : ℝ) :
   has_finite_integral (λ x, f x * c) μ :=
 by simp_rw [mul_comm, h.const_mul _]
+
 end normed_space
 
 /-! ### The predicate `integrable` -/
@@ -557,6 +573,19 @@ begin
   simp [real.norm_eq_abs, ennreal.of_real_le_of_real, abs_le, abs_nonneg, le_abs_self],
 end
 
+lemma mem_ℒ1_to_real_of_lintegral_ne_top
+  {f : α → ℝ≥0∞} (hfm : ae_measurable f μ) (hfi : ∫⁻ x, f x ∂μ ≠ ∞) :
+  mem_ℒp (λ x, (f x).to_real) 1 μ :=
+begin
+  rw [mem_ℒp, snorm_one_eq_lintegral_nnnorm],
+  exact ⟨ae_measurable.ennreal_to_real hfm, has_finite_integral_to_real_of_lintegral_ne_top hfi⟩
+end
+
+lemma integrable_to_real_of_lintegral_ne_top
+  {f : α → ℝ≥0∞} (hfm : ae_measurable f μ) (hfi : ∫⁻ x, f x ∂μ ≠ ∞) :
+  integrable (λ x, (f x).to_real) μ :=
+mem_ℒp_one_iff_integrable.1 $ mem_ℒ1_to_real_of_lintegral_ne_top hfm hfi
+
 section pos_part
 /-! ### Lemmas used for defining the positive part of a `L¹` function -/
 

src/measure_theory/measure/with_density_vector_measure.lean

@@ -74,6 +74,9 @@ begin
     rwa integrable_neg_iff }
 end
 
+lemma with_densityᵥ_neg' : μ.with_densityᵥ (λ x, -f x) = -μ.with_densityᵥ f :=
+with_densityᵥ_neg
+
 @[simp] lemma with_densityᵥ_add (hf : integrable f μ) (hg : integrable g μ) :
   μ.with_densityᵥ (f + g) = μ.with_densityᵥ f + μ.with_densityᵥ g :=
 begin
@@ -86,10 +89,18 @@ begin
   { exact hg.integrable_on.restrict measurable_set.univ }
 end
 
+lemma with_densityᵥ_add' (hf : integrable f μ) (hg : integrable g μ) :
+  μ.with_densityᵥ (λ x, f x + g x) = μ.with_densityᵥ f + μ.with_densityᵥ g :=
+with_densityᵥ_add hf hg
+
 @[simp] lemma with_densityᵥ_sub (hf : integrable f μ) (hg : integrable g μ) :
   μ.with_densityᵥ (f - g) = μ.with_densityᵥ f - μ.with_densityᵥ g :=
 by rw [sub_eq_add_neg, sub_eq_add_neg, with_densityᵥ_add hf hg.neg, with_densityᵥ_neg]
 
+lemma with_densityᵥ_sub' (hf : integrable f μ) (hg : integrable g μ) :
+  μ.with_densityᵥ (λ x, f x - g x) = μ.with_densityᵥ f - μ.with_densityᵥ g :=
+with_densityᵥ_sub hf hg
+
 @[simp] lemma with_densityᵥ_smul {𝕜 : Type*} [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E]
   [smul_comm_class ℝ 𝕜 E] [measurable_space 𝕜] [opens_measurable_space 𝕜] (r : 𝕜) :
   μ.with_densityᵥ (r • f) = r • μ.with_densityᵥ f :=
@@ -105,6 +116,11 @@ begin
       rwa integrable_smul_iff hr f } }
 end
 
+lemma with_densityᵥ_smul' {𝕜 : Type*} [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E]
+  [smul_comm_class ℝ 𝕜 E] [measurable_space 𝕜] [opens_measurable_space 𝕜] (r : 𝕜) :
+  μ.with_densityᵥ (λ x, r • f x) = r • μ.with_densityᵥ f :=
+with_densityᵥ_smul r
+
 lemma measure.with_densityᵥ_absolutely_continuous (μ : measure α) (f : α → ℝ) :
   μ.with_densityᵥ f ≪ μ.to_ennreal_vector_measure :=
 begin
@@ -144,6 +160,20 @@ lemma integrable.with_densityᵥ_eq_iff {f g : α → E}
 
 section signed_measure
 
+lemma with_densityᵥ_to_real {f : α → ℝ≥0∞} (hfm : ae_measurable f μ) (hf : ∫⁻ x, f x ∂μ ≠ ∞) :
+  μ.with_densityᵥ (λ x, (f x).to_real) =
+  @to_signed_measure α _ (μ.with_density f)
+    (is_finite_measure_with_density (lt_top_iff_ne_top.2 hf)) :=
+begin
+  have hfi := integrable_to_real_of_lintegral_ne_top hfm hf,
+  ext i hi,
+  rw [with_densityᵥ_apply hfi hi, to_signed_measure_apply_measurable hi,
+      with_density_apply _ hi, integral_to_real hfm.restrict],
+  refine ae_lt_top' hfm.restrict (lt_of_le_of_lt _ (lt_top_iff_ne_top.2 hf)),
+  conv_rhs { rw ← set_lintegral_univ },
+  exact lintegral_mono_set (set.subset_univ _),
+end
+
 lemma with_densityᵥ_eq_with_density_pos_part_sub_with_density_neg_part
   {f : α → ℝ} (hfi : integrable f μ) :
   μ.with_densityᵥ f =