bochner integral over set of measure zero is zero

Stream: Is there code for X?

[Pietro Lavino]

I have an integral of the form

$$\int x in A, f x \partial \mu$$

where

$$\mu A = 0$$

is there a theorem stating that the integral must be zero, can't seem to find it

[Daniel Weber]

Is docs#MeasureTheory.integral_eq_zero_of_ae what you want? EDIT: nvm, I mistunderstood

[Daniel Weber]

You should be able to conclude this from docs#MeasureTheory.setIntegral_eq_zero_of_ae_eq_zero

[Sébastien Gouëzel]

I haven't found it exactly, but it's pretty quick:

theorem setIntegral_eq_zero_of_measure_eq_zero (ht : μ t = 0) :
    ∫ x in t, f x ∂μ = 0 := by
  simp [Measure.restrict_eq_zero.mpr ht]

PR welcome!