# Properties of integration with respect to the Lebesgue measure #

source
theorem volume_regionBetween_eq_integral' {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ℝ} {s : Set α} [MeasureTheory.SigmaFinite μ] (f_int : MeasureTheory.IntegrableOn f s μ) (g_int : MeasureTheory.IntegrableOn g s μ) (hs : MeasurableSet s) (hfg : f ≤ᵐ[μ.restrict s] g) :
(μ.prod MeasureTheory.volume) (regionBetween f g s) = ENNReal.ofReal (∫ (y : α) in s, (g - f) y ∂μ)
source
theorem volume_regionBetween_eq_integral {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ℝ} {s : Set α} [MeasureTheory.SigmaFinite μ] (f_int : MeasureTheory.IntegrableOn f s μ) (g_int : MeasureTheory.IntegrableOn g s μ) (hs : MeasurableSet s) (hfg : ∀ x ∈ s, f x ≤ g x) :
(μ.prod MeasureTheory.volume) (regionBetween f g s) = ENNReal.ofReal (∫ (y : α) in s, (g - f) y ∂μ)

If two functions are integrable on a measurable set, and one function is less than or equal to the other on that set, then the volume of the region between the two functions can be represented as an integral.

source
theorem Real.integrable_of_summable_norm_Icc {E : Type u_1} [NormedAddCommGroup E] {f : C(ℝ, E)} (hf : Summable fun (n : ℤ) => ‖ContinuousMap.restrict (Set.Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))‖) :
MeasureTheory.Integrable (⇑f) MeasureTheory.volume

If the sequence with `n`-th term the sup norm of `fun x ↦ f (x + n)` on the interval `Icc 0 1`, for `n ∈ ℤ`, is summable, then `f` is integrable on `ℝ`.

### Substituting `-x` for `x` #

These lemmas are stated in terms of either `Iic` or `Ioi` (neglecting `Iio` and `Ici`) to match mathlib's conventions for integrals over finite intervals (see `intervalIntegral`). For the case of finite integrals, see `intervalIntegral.integral_comp_neg`.

source
@[simp]
theorem integral_comp_neg_Iic {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (c : ℝ) (f : ℝ → E) :
∫ (x : ℝ) in Set.Iic c, f (-x) = ∫ (x : ℝ) in Set.Ioi (-c), f x
source
@[simp]
theorem integral_comp_neg_Ioi {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (c : ℝ) (f : ℝ → E) :
∫ (x : ℝ) in Set.Ioi c, f (-x) = ∫ (x : ℝ) in Set.Iic (-c), f x
source
theorem integral_comp_abs {f : ℝ → ℝ} :
∫ (x : ℝ), f |x| = 2 * ∫ (x : ℝ) in Set.Ioi 0, f x