feat(measure_theory): assorted integration lemmas (#4145)

from the sphere eversion project

This is still preparations for differentiation of integals depending on a parameter.

Author: PatrickMassot

src/measure_theory/bochner_integration.lean

@@ -903,6 +903,10 @@ calc ∥integral f∥ = ∥Integral f∥ : rfl
   ... ≤ 1 * ∥f∥ : mul_le_mul_of_nonneg_right norm_Integral_le_one $ norm_nonneg _
   ... = ∥f∥ : one_mul _
 
+@[continuity]
+lemma continuous_integral : continuous (λ (f : α →₁[μ] E), f.integral) :=
+by simp [l1.integral, l1.integral_clm.continuous]
+
 section pos_part
 
 lemma integral_eq_norm_pos_part_sub (f : α →₁[μ] ℝ) : integral f = ∥pos_part f∥ - ∥neg_part f∥ :=
@@ -953,6 +957,9 @@ lemma integral_eq (f : α → E) (h₁ : measurable f) (h₂ : integrable f μ)
   ∫ a, f a ∂μ = (l1.of_fun f h₁ h₂).integral :=
 dif_pos ⟨h₁, h₂⟩
 
+lemma l1.integral_eq_integral (f : α →₁[μ] E) : f.integral = ∫ a, f a ∂μ :=
+by rw [integral_eq, l1.of_fun_to_fun]
+
 lemma integral_undef (h : ¬ (measurable f ∧ integrable f μ)) : ∫ a, f a ∂μ = 0 :=
 dif_neg h
 
@@ -1018,6 +1025,18 @@ begin
     rw [integral_non_integrable hfi, integral_non_integrable hgi] },
 end
 
+@[simp] lemma l1.integral_of_fun_eq_integral {f : α → E} (f_m : measurable f) (f_i : integrable f μ) :
+  ∫ a, (l1.of_fun f f_m f_i) a ∂μ = ∫ a, f a ∂μ :=
+integral_congr_ae (l1.measurable _) f_m (l1.to_fun_of_fun f f_m f_i)
+
+@[continuity]
+lemma continuous_integral : continuous (λ (f : α →₁[μ] E), ∫ a, f a ∂μ) :=
+begin
+  convert l1.continuous_integral,
+  ext f,
+  rw l1.integral_eq_integral
+end
+
 lemma norm_integral_le_lintegral_norm (f : α → E) :
   ∥∫ a, f a ∂μ∥ ≤ ennreal.to_real (∫⁻ a, (ennreal.of_real ∥f a∥) ∂μ) :=
 begin
@@ -1186,6 +1205,27 @@ begin
   rwa [integral_neg, neg_nonneg] at this,
 end
 
+section normed_group
+variables {H : Type*} [normed_group H] [second_countable_topology H] [measurable_space H]
+          [borel_space H]
+
+lemma l1.norm_eq_integral_norm (f : α →₁[μ] H) : ∥f∥ = ∫ a, ∥f a∥ ∂μ :=
+by rw [l1.norm_eq_norm_to_fun,
+       integral_eq_lintegral_of_nonneg_ae (eventually_of_forall $ by simp [norm_nonneg])
+       (continuous_norm.measurable.comp f.measurable)]
+
+lemma l1.norm_of_fun_eq_integral_norm {f : α → H} (f_m : measurable f) (f_i : integrable f μ) :
+  ∥l1.of_fun f f_m f_i∥ = ∫ a, ∥f a∥ ∂μ :=
+begin
+  rw l1.norm_eq_integral_norm,
+  refine integral_congr_ae (l1.measurable_norm _) f_m.norm _,
+  apply (l1.to_fun_of_fun f f_m f_i).mono,
+  intros a ha,
+  simp [ha]
+end
+
+end normed_group
+
 lemma integral_mono {f g : α → ℝ} (hfm : measurable f) (hfi : integrable f μ)
   (hgm : measurable g) (hgi : integrable g μ) (h : f ≤ᵐ[μ] g) : ∫ a, f a ∂μ ≤ ∫ a, g a ∂μ :=
 le_of_sub_nonneg $ integral_sub hgm hgi hfm hfi ▸

src/measure_theory/borel_space.lean

@@ -497,6 +497,17 @@ instance nnreal.borel_space : borel_space nnreal := ⟨rfl⟩
 instance ennreal.measurable_space : measurable_space ennreal := borel ennreal
 instance ennreal.borel_space : borel_space ennreal := ⟨rfl⟩
 
+section real_mul
+variables [measurable_space α]
+
+lemma measurable.const_mul {f : α → ℝ} (h : measurable f) (c : ℝ) : measurable (λ x, c*f x) :=
+(measurable.const_smul h c : _)
+
+lemma measurable.mul_const {f : α → ℝ} (h : measurable f) (c : ℝ) : measurable (λ x, f x*c) :=
+by simp only [h.const_mul c, mul_comm]
+
+end real_mul
+
 section metric_space
 
 variables [metric_space α] [measurable_space α] [opens_measurable_space α] {x : α} {ε : ℝ}
@@ -704,6 +715,22 @@ hf.nnnorm.ennreal_coe
 
 end normed_group
 
+section normed_space
+
+variables [measurable_space α]
+variables {𝕜 : Type*} [normed_field 𝕜]
+variables {E : Type*} [normed_group E] [normed_space 𝕜 E] [measurable_space E] [borel_space E]
+variables {F : Type*} [normed_group F] [normed_space 𝕜 F] [measurable_space F] [borel_space F]
+
+lemma continuous_linear_map.measurable (L : E →L[𝕜] F) : measurable L :=
+L.continuous.measurable
+
+lemma measurable.clm_apply {φ : α → E} (φ_meas : measurable φ)
+  (L : E →L[𝕜] F) : measurable (λ (a : α), L (φ a)) :=
+L.measurable.comp φ_meas
+
+end normed_space
+
 namespace measure_theory
 namespace measure
 

src/measure_theory/l1_space.lean

@@ -395,6 +395,12 @@ begin
   exact integrable.smul _
 end
 
+lemma integrable.const_mul {f : α → ℝ} (h : integrable f μ) (c : ℝ) : integrable (λ x, c * f x) μ :=
+(integrable.smul c h : _)
+
+lemma integrable.mul_const {f : α → ℝ} (h : integrable f μ) (c : ℝ) : integrable (λ x, f x * c) μ :=
+by simp_rw [mul_comm, h.const_mul _]
+
 end normed_space
 
 variables [second_countable_topology β]
@@ -604,9 +610,15 @@ section to_fun
 
 protected lemma measurable (f : α →₁[μ] β) : measurable f := f.1.measurable
 
+lemma measurable_norm (f : α →₁[μ] β) : measurable (λ a, ∥f a∥) :=
+f.measurable.norm
+
 protected lemma integrable (f : α →₁[μ] β) : integrable ⇑f μ :=
 integrable_coe_fn.2 f.2
 
+lemma integrable_norm (f : α →₁[μ] β) : integrable (λ a, ∥f a∥) μ :=
+(integrable_norm_iff _).mpr f.integrable
+
 lemma of_fun_to_fun (f : α →₁[μ] β) : of_fun f f.measurable f.integrable = f :=
 subtype.ext (f : α →ₘ[μ] β).mk_coe_fn
 

src/measure_theory/set_integral.lean

@@ -352,6 +352,11 @@ by { rwa [integral_non_integrable, integral_non_integrable], rwa integrable_indi
 lemma set_integral_const (c : E) : ∫ x in s, c ∂μ = (μ s).to_real • c :=
 by rw [integral_const, measure.restrict_apply_univ]
 
+@[simp]
+lemma integral_indicator_const (e : E) ⦃s : set α⦄ (s_meas : is_measurable s) :
+  ∫ (a : α), s.indicator (λ (x : α), e) a ∂μ = (μ s).to_real • e :=
+by rw [integral_indicator measurable_const s_meas, ← set_integral_const]
+
 lemma norm_set_integral_le_of_norm_le_const_ae {C : ℝ} (hs : μ s < ⊤)
   (hC : ∀ᵐ x ∂μ.restrict s, ∥f x∥ ≤ C) :
   ∥∫ x in s, f x ∂μ∥ ≤ C * (μ s).to_real :=