chore(measure_theory/integral/interval_integral): generalize `integra…

…l_smul` (#9355) Make sure that it works for scalar multiplication by a complex number.
leanprover-community · Sep 24, 2021 · 18f06ec · 18f06ec
1 parent 7cb7246
commit 18f06ec
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 2 deletions.
diff --git a/src/analysis/special_functions/integrals.lean b/src/analysis/special_functions/integrals.lean
@@ -115,7 +115,7 @@ by simpa only [one_div] using interval_integrable_one_div_one_add_sq
 
 @[simp]
 lemma integral_const_mul : ∫ x in a..b, c * f x = c * ∫ x in a..b, f x :=
-integral_smul c
+integral_smul c f
 
 @[simp]
 lemma integral_mul_const : ∫ x in a..b, f x * c = (∫ x in a..b, f x) * c :=

diff --git a/src/measure_theory/integral/interval_integral.lean b/src/measure_theory/integral/interval_integral.lean
@@ -547,7 +547,9 @@ by { simp only [interval_integral, integral_neg], abel }
   ∫ x in a..b, f x - g x ∂μ = ∫ x in a..b, f x ∂μ - ∫ x in a..b, g x ∂μ :=
 by simpa only [sub_eq_add_neg] using (integral_add hf hg.neg).trans (congr_arg _ integral_neg)
 
-@[simp] lemma integral_smul (r : ℝ) : ∫ x in a..b, r • f x ∂μ = r • ∫ x in a..b, f x ∂μ :=
+@[simp] lemma integral_smul {𝕜 : Type*} [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E]
+  [smul_comm_class ℝ 𝕜 E] [measurable_space 𝕜] [opens_measurable_space 𝕜]
+  (r : 𝕜) (f : α → E) : ∫ x in a..b, r • f x ∂μ = r • ∫ x in a..b, f x ∂μ :=
 by simp only [interval_integral, integral_smul, smul_sub]
 
 lemma integral_const' (c : E) :