Smul Set.integral

Stream: Is there code for X?

[Josha Dekker]

Is there a theorem like MeasureTheory.integral_smul but for set integrals? I just want to pull out the constant b in the following:

import Mathlib.Analysis.SpecialFunctions.Gaussian
open scoped ENNReal NNReal Real


open MeasureTheory Set

lemma test {a r : ℝ} (ha : a > 0) (hb : b > 0) : ∫ (t : ℝ) in Ioi 0, b • t ^ (a - 1) * rexp (-t) =  b • (∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * rexp (-t))
    := by sorry

[Yaël Dillies]

MeasureTheory.integral_smul will work

[Yaël Dillies]

A set integral is such notation under integral, so all lemmas that apply to integral will work on it (except that some might turn your set integral into something which is not of the form of a set integral).

[Josha Dekker]

Yes, that is what I thought as well, so I tried it, but it says that it can't unify the two; perhaps I'm doing something wrong, let me check

[Yaël Dillies]

You should rewrite docs#smul_mul_assoc inside the integrand for it to apply.

[Rémy Degenne]

To expand on the answer of Yaël: the issue is that you don't have b • (t ^ (a - 1) * rexp (-t)) under the integral, you have (b • t ^ (a - 1)) * rexp (-t).

[Josha Dekker]

Thanks, that explains it!