feat(measure_theory/integral): "integral_prod_mul" for complex coeffi…

…cients (#18085)

This generalises some lemmas in the integration library, currently only stated for `ℝ`-valued functions, to allow complex-valued functions too. (Note that one can't generalise all the way to an arbitrary Banach algebra, there are problems when one side is integrable and the other isn't.)

src/measure_theory/constructions/prod.lean

@@ -904,7 +904,8 @@ lemma integrable.integral_norm_prod_right [sigma_finite μ] ⦃f : α × β →
   (hf : integrable f (μ.prod ν)) : integrable (λ y, ∫ x, ‖f (x, y)‖ ∂μ) ν :=
 hf.swap.integral_norm_prod_left
 
-lemma integrable_prod_mul {f : α → ℝ} {g : β → ℝ} (hf : integrable f μ) (hg : integrable g ν) :
+lemma integrable_prod_mul {L : Type*} [is_R_or_C L]
+  {f : α → L} {g : β → L} (hf : integrable f μ) (hg : integrable g ν) :
   integrable (λ (z : α × β), f z.1 * g z.2) (μ.prod ν) :=
 begin
   refine (integrable_prod_iff _).2 ⟨_, _⟩,
@@ -1083,7 +1084,7 @@ begin
   exact integral_prod f hf
 end
 
-lemma integral_prod_mul (f : α → ℝ) (g : β → ℝ) :
+lemma integral_prod_mul {L : Type*} [is_R_or_C L] (f : α → L) (g : β → L) :
   ∫ z, f z.1 * g z.2 ∂(μ.prod ν) = (∫ x, f x ∂μ) * (∫ y, g y ∂ν) :=
 begin
   by_cases h : integrable (λ (z : α × β), f z.1 * g z.2) (μ.prod ν),
@@ -1096,7 +1097,8 @@ begin
   simp [integral_undef h, integral_undef H],
 end
 
-lemma set_integral_prod_mul (f : α → ℝ) (g : β → ℝ) (s : set α) (t : set β) :
+lemma set_integral_prod_mul {L : Type*} [is_R_or_C L]
+  (f : α → L) (g : β → L) (s : set α) (t : set β) :
   ∫ z in s ×ˢ t, f z.1 * g z.2 ∂(μ.prod ν) = (∫ x in s, f x ∂μ) * (∫ y in t, g y ∂ν) :=
 by simp only [← measure.prod_restrict s t, integrable_on, integral_prod_mul]
 

src/measure_theory/function/l1_space.lean

@@ -882,27 +882,47 @@ lemma integrable_smul_iff {c : 𝕜} (hc : c ≠ 0) (f : α → β) :
   integrable (c • f) μ ↔ integrable f μ :=
 and_congr (ae_strongly_measurable_const_smul_iff₀ hc) (has_finite_integral_smul_iff hc f)
 
-lemma integrable.const_mul {f : α → ℝ} (h : integrable f μ) (c : ℝ) :
+end normed_space
+
+section normed_space_over_complete_field
+variables {𝕜 : Type*} [nontrivially_normed_field 𝕜] [complete_space 𝕜]
+variables {E : Type*} [normed_add_comm_group E] [normed_space 𝕜 E]
+
+lemma integrable_smul_const {f : α → 𝕜} {c : E} (hc : c ≠ 0) :
+  integrable (λ x, f x • c) μ ↔ integrable f μ :=
+begin
+  simp_rw [integrable, ae_strongly_measurable_smul_const_iff hc, and.congr_right_iff,
+    has_finite_integral, nnnorm_smul, ennreal.coe_mul],
+  intro hf, rw [lintegral_mul_const' _ _ ennreal.coe_ne_top, ennreal.mul_lt_top_iff],
+  have : ∀ x : ℝ≥0∞, x = 0 → x < ∞ := by simp,
+  simp [hc, or_iff_left_of_imp (this _)]
+end
+end normed_space_over_complete_field
+
+section is_R_or_C
+variables {𝕜 : Type*} [is_R_or_C 𝕜] {f : α → 𝕜}
+
+lemma integrable.const_mul {f : α → 𝕜} (h : integrable f μ) (c : 𝕜) :
   integrable (λ x, c * f x) μ :=
 integrable.smul c h
 
-lemma integrable.const_mul' {f : α → ℝ} (h : integrable f μ) (c : ℝ) :
+lemma integrable.const_mul' {f : α → 𝕜} (h : integrable f μ) (c : 𝕜) :
   integrable ((λ (x : α), c) * f) μ :=
 integrable.smul c h
 
-lemma integrable.mul_const {f : α → ℝ} (h : integrable f μ) (c : ℝ) :
+lemma integrable.mul_const {f : α → 𝕜} (h : integrable f μ) (c : 𝕜) :
   integrable (λ x, f x * c) μ :=
 by simp_rw [mul_comm, h.const_mul _]
 
-lemma integrable.mul_const' {f : α → ℝ} (h : integrable f μ) (c : ℝ) :
+lemma integrable.mul_const' {f : α → 𝕜} (h : integrable f μ) (c : 𝕜) :
   integrable (f * (λ (x : α), c)) μ :=
 integrable.mul_const h c
 
-lemma integrable.div_const {f : α → ℝ} (h : integrable f μ) (c : ℝ) :
+lemma integrable.div_const {f : α → 𝕜} (h : integrable f μ) (c : 𝕜) :
   integrable (λ x, f x / c) μ :=
 by simp_rw [div_eq_mul_inv, h.mul_const]
 
-lemma integrable.bdd_mul' {f g : α → ℝ} {c : ℝ} (hg : integrable g μ)
+lemma integrable.bdd_mul' {f g : α → 𝕜} {c : ℝ} (hg : integrable g μ)
   (hf : ae_strongly_measurable f μ) (hf_bound : ∀ᵐ x ∂μ, ‖f x‖ ≤ c) :
   integrable (λ x, f x * g x) μ :=
 begin
@@ -912,26 +932,6 @@ begin
   exact (norm_mul_le _ _).trans (mul_le_mul_of_nonneg_right hx (norm_nonneg _)),
 end
 
-end normed_space
-
-section normed_space_over_complete_field
-variables {𝕜 : Type*} [nontrivially_normed_field 𝕜] [complete_space 𝕜]
-variables {E : Type*} [normed_add_comm_group E] [normed_space 𝕜 E]
-
-lemma integrable_smul_const {f : α → 𝕜} {c : E} (hc : c ≠ 0) :
-  integrable (λ x, f x • c) μ ↔ integrable f μ :=
-begin
-  simp_rw [integrable, ae_strongly_measurable_smul_const_iff hc, and.congr_right_iff,
-    has_finite_integral, nnnorm_smul, ennreal.coe_mul],
-  intro hf, rw [lintegral_mul_const' _ _ ennreal.coe_ne_top, ennreal.mul_lt_top_iff],
-  have : ∀ x : ℝ≥0∞, x = 0 → x < ∞ := by simp,
-  simp [hc, or_iff_left_of_imp (this _)]
-end
-end normed_space_over_complete_field
-
-section is_R_or_C
-variables {𝕜 : Type*} [is_R_or_C 𝕜] {f : α → 𝕜}
-
 lemma integrable.of_real {f : α → ℝ} (hf : integrable f μ) :
   integrable (λ x, (f x : 𝕜)) μ :=
 by { rw ← mem_ℒp_one_iff_integrable at hf ⊢, exact hf.of_real }

src/measure_theory/integral/bochner.lean

@@ -770,14 +770,17 @@ lemma integral_smul (c : 𝕜) (f : α → E) :
   ∫ a, c • (f a) ∂μ = c • ∫ a, f a ∂μ :=
 set_to_fun_smul (dominated_fin_meas_additive_weighted_smul μ) weighted_smul_smul c f
 
-lemma integral_mul_left (r : ℝ) (f : α → ℝ) : ∫ a, r * (f a) ∂μ = r * ∫ a, f a ∂μ :=
+lemma integral_mul_left {L : Type*} [is_R_or_C L] (r : L) (f : α → L) :
+  ∫ a, r * (f a) ∂μ = r * ∫ a, f a ∂μ :=
 integral_smul r f
 
-lemma integral_mul_right (r : ℝ) (f : α → ℝ) : ∫ a, (f a) * r ∂μ = ∫ a, f a ∂μ * r :=
+lemma integral_mul_right {L : Type*} [is_R_or_C L] (r : L) (f : α → L) :
+  ∫ a, (f a) * r ∂μ = ∫ a, f a ∂μ * r :=
 by { simp only [mul_comm], exact integral_mul_left r f }
 
-lemma integral_div (r : ℝ) (f : α → ℝ) : ∫ a, (f a) / r ∂μ = ∫ a, f a ∂μ / r :=
-integral_mul_right r⁻¹ f
+lemma integral_div {L : Type*} [is_R_or_C L] (r : L) (f : α → L) :
+  ∫ a, (f a) / r ∂μ = ∫ a, f a ∂μ / r :=
+by simpa only [←div_eq_mul_inv] using integral_mul_right r⁻¹ f
 
 lemma integral_congr_ae (h : f =ᵐ[μ] g) : ∫ a, f a ∂μ = ∫ a, g a ∂μ :=
 set_to_fun_congr_ae (dominated_fin_meas_additive_weighted_smul μ) h

src/probability/variance.lean

@@ -362,7 +362,7 @@ begin
       { apply mem_ℒp.integrable_sq,
         exact mem_ℒp_finset_sum' _ (λ i hi, (hs _ (mem_insert_of_mem hi))) } },
     { rw mul_assoc,
-      apply integrable.const_mul _ 2,
+      apply integrable.const_mul _ (2:ℝ),
       simp only [mul_sum, sum_apply, pi.mul_apply],
       apply integrable_finset_sum _ (λ i hi, _),
       apply indep_fun.integrable_mul _
@@ -383,7 +383,7 @@ begin
     simp only [mul_assoc, integral_mul_left, pi.mul_apply, pi.bit0_apply, pi.one_apply, sum_apply,
       add_right_eq_self, mul_sum],
     rw integral_finset_sum s (λ i hi, _), swap,
-    { apply integrable.const_mul _ 2,
+    { apply integrable.const_mul _ (2:ℝ),
       apply indep_fun.integrable_mul _
         (mem_ℒp.integrable one_le_two (hs _ (mem_insert_self _ _)))
         (mem_ℒp.integrable one_le_two (hs _ (mem_insert_of_mem hi))),