feat(measure_theory/integral/lebesgue): weaken assumptions for with_density lemmas (#11711)

We state more precise versions of some lemmas about the measure `μ.with_density f`, making it possible to remove some assumptions down the road. For instance, the lemma
```lean
  integrable g (μ.with_density f) ↔ integrable (λ x, g x * (f x).to_real) μ
```
currently requires the measurability of `g`, while we can completely remove it with the new lemmas.

We also make `lintegral` irreducible.

Author: sgouezel

src/measure_theory/constructions/borel_space.lean

@@ -1810,6 +1810,23 @@ begin
   { exact tendsto_const_nhds, },
 end
 
+lemma ae_measurable_of_unif_approx {μ : measure α} {g : α → β}
+  (hf : ∀ ε > (0 : ℝ), ∃ (f : α → β), ae_measurable f μ ∧ ∀ᵐ x ∂μ, dist (f x) (g x) ≤ ε) :
+  ae_measurable g μ :=
+begin
+  obtain ⟨u, u_anti, u_pos, u_lim⟩ :
+    ∃ (u : ℕ → ℝ), strict_anti u ∧ (∀ (n : ℕ), 0 < u n) ∧ tendsto u at_top (𝓝 0) :=
+      exists_seq_strict_anti_tendsto (0 : ℝ),
+  choose f Hf using λ (n : ℕ), hf (u n) (u_pos n),
+  have : ∀ᵐ x ∂μ, tendsto (λ n, f n x) at_top (𝓝 (g x)),
+  { have : ∀ᵐ x ∂ μ, ∀ n, dist (f n x) (g x) ≤ u n := ae_all_iff.2 (λ n, (Hf n).2),
+    filter_upwards [this],
+    assume x hx,
+    rw tendsto_iff_dist_tendsto_zero,
+    exact squeeze_zero (λ n, dist_nonneg) hx u_lim },
+  exact ae_measurable_of_tendsto_metric_ae (λ n, (Hf n).1) this,
+end
+
 lemma measurable_of_tendsto_metric_ae {μ : measure α} [μ.is_complete] {f : ℕ → α → β} {g : α → β}
   (hf : ∀ n, measurable (f n))
   (h_ae_tendsto : ∀ᵐ x ∂μ, filter.at_top.tendsto (λ n, f n x) (𝓝 (g x))) :

src/measure_theory/function/ae_eq_of_integral.lean

@@ -307,7 +307,7 @@ lemma ae_fin_strongly_measurable.ae_nonneg_of_forall_set_integral_nonneg {f : α
 begin
   let t := hf.sigma_finite_set,
   suffices : 0 ≤ᵐ[μ.restrict t] f,
-    from ae_of_ae_restrict_of_ae_restrict_compl this hf.ae_eq_zero_compl.symm.le,
+    from ae_of_ae_restrict_of_ae_restrict_compl _ this hf.ae_eq_zero_compl.symm.le,
   haveI : sigma_finite (μ.restrict t) := hf.sigma_finite_restrict,
   refine ae_nonneg_of_forall_set_integral_nonneg_of_sigma_finite (λ s hs hμts, _)
     (λ s hs hμts, _),
@@ -432,7 +432,7 @@ lemma ae_fin_strongly_measurable.ae_eq_zero_of_forall_set_integral_eq_zero {f :
 begin
   let t := hf.sigma_finite_set,
   suffices : f =ᵐ[μ.restrict t] 0,
-    from ae_of_ae_restrict_of_ae_restrict_compl this hf.ae_eq_zero_compl,
+    from ae_of_ae_restrict_of_ae_restrict_compl _ this hf.ae_eq_zero_compl,
   haveI : sigma_finite (μ.restrict t) := hf.sigma_finite_restrict,
   refine ae_eq_zero_of_forall_set_integral_eq_of_sigma_finite _ _,
   { intros s hs hμs,
@@ -492,7 +492,7 @@ begin
     exact eventually_of_forall htf_zero, },
   have hf_meas_m : @measurable _ _ m _ f, from hf.measurable,
   suffices : f =ᵐ[μ.restrict t] 0,
-    from ae_of_ae_restrict_of_ae_restrict_compl this htf_zero,
+    from ae_of_ae_restrict_of_ae_restrict_compl _ this htf_zero,
   refine measure_eq_zero_of_trim_eq_zero hm _,
   refine ae_eq_zero_of_forall_set_integral_eq_of_sigma_finite _ _,
   { intros s hs hμs,

src/measure_theory/function/l1_space.lean

@@ -592,34 +592,57 @@ end
 lemma of_real_to_real_ae_eq {f : α → ℝ≥0∞} (hf : ∀ᵐ x ∂μ, f x < ∞) :
   (λ x, ennreal.of_real (f x).to_real) =ᵐ[μ] f :=
 begin
-  rw ae_iff at hf,
-  rw [filter.eventually_eq, ae_iff],
-  have : {x | ¬ ennreal.of_real (f x).to_real = f x} = {x | f x = ∞},
-  { ext x,
-    simp only [ne.def, set.mem_set_of_eq],
-    split; intro hx,
-    { by_contra hntop,
-      exact hx (ennreal.of_real_to_real hntop) },
-    { rw hx, simp } },
-  rw this,
-  simpa using hf,
+  filter_upwards [hf],
+  assume x hx,
+  simp only [hx.ne, of_real_to_real, ne.def, not_false_iff],
+end
+
+lemma coe_to_nnreal_ae_eq {f : α → ℝ≥0∞} (hf : ∀ᵐ x ∂μ, f x < ∞) :
+  (λ x, ((f x).to_nnreal : ℝ≥0∞)) =ᵐ[μ] f :=
+begin
+  filter_upwards [hf],
+  assume x hx,
+  simp only [hx.ne, ne.def, not_false_iff, coe_to_nnreal],
+end
+
+lemma integrable_with_density_iff_integrable_smul
+  {E : Type*} [normed_group E] [normed_space ℝ E] [second_countable_topology E]
+  [measurable_space E] [borel_space E]
+  {f : α → ℝ≥0} (hf : measurable f) {g : α → E} :
+  integrable g (μ.with_density (λ x, (f x : ℝ≥0∞))) ↔ integrable (λ x, (f x : ℝ) • g x) μ :=
+begin
+  by_cases H : ae_measurable (λ (x : α), (f x : ℝ) • g x) μ,
+  { simp only [integrable, ae_measurable_with_density_iff hf, has_finite_integral, H, true_and],
+    rw lintegral_with_density_eq_lintegral_mul₀' hf.coe_nnreal_ennreal.ae_measurable,
+    { congr',
+      ext1 x,
+      simp only [nnnorm_smul, nnreal.nnnorm_eq, coe_mul, pi.mul_apply] },
+    { rw ae_measurable_with_density_ennreal_iff hf,
+      convert H.nnnorm.coe_nnreal_ennreal,
+      ext1 x,
+      simp only [nnnorm_smul, nnreal.nnnorm_eq, coe_mul] } },
+  { simp only [integrable, ae_measurable_with_density_iff hf, H, false_and] }
+end
+
+lemma integrable_with_density_iff_integrable_smul'
+  {E : Type*} [normed_group E] [normed_space ℝ E] [second_countable_topology E]
+  [measurable_space E] [borel_space E]
+  {f : α → ℝ≥0∞} (hf : measurable f) (hflt : ∀ᵐ x ∂μ, f x < ∞) {g : α → E} :
+  integrable g (μ.with_density f) ↔ integrable (λ x, (f x).to_real • g x) μ :=
+begin
+  rw [← with_density_congr_ae (coe_to_nnreal_ae_eq hflt),
+      integrable_with_density_iff_integrable_smul],
+  { refl },
+  { exact hf.ennreal_to_nnreal },
 end
 
 lemma integrable_with_density_iff {f : α → ℝ≥0∞} (hf : measurable f)
-  (hflt : ∀ᵐ x ∂μ, f x < ∞) {g : α → ℝ} (hg : measurable g) :
+  (hflt : ∀ᵐ x ∂μ, f x < ∞) {g : α → ℝ} :
   integrable g (μ.with_density f) ↔ integrable (λ x, g x * (f x).to_real) μ :=
 begin
-  simp only [integrable, has_finite_integral, hg.ae_measurable.mul hf.ae_measurable.ennreal_to_real,
-    hg.ae_measurable, true_and, coe_mul, normed_field.nnnorm_mul],
-  suffices h_int_eq : ∫⁻ a, ∥g a∥₊ ∂μ.with_density f = ∫⁻ a, ∥g a∥₊ * ∥(f a).to_real∥₊ ∂μ,
-    by rw h_int_eq,
-  rw lintegral_with_density_eq_lintegral_mul _ hf hg.nnnorm.coe_nnreal_ennreal,
-  refine lintegral_congr_ae _,
-  rw mul_comm,
-  refine filter.eventually_eq.mul (ae_eq_refl _) ((of_real_to_real_ae_eq hflt).symm.trans _),
-  convert ae_eq_refl _,
-  ext1 x,
-  exact real.ennnorm_eq_of_real ennreal.to_real_nonneg,
+  have : (λ x, g x * (f x).to_real) = (λ x, (f x).to_real • g x), by simp [mul_comm],
+  rw this,
+  exact integrable_with_density_iff_integrable_smul' hf hflt,
 end
 
 lemma mem_ℒ1_to_real_of_lintegral_ne_top