Properties of integration with respect to the Lebesgue measure #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
theorem
volume_region_between_eq_integral'
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f g : α → ℝ}
{s : set α}
[measure_theory.sigma_finite μ]
(f_int : measure_theory.integrable_on f s μ)
(g_int : measure_theory.integrable_on g s μ)
(hs : measurable_set s)
(hfg : f ≤ᵐ[μ.restrict s] g) :
⇑(μ.prod measure_theory.measure_space.volume) (region_between f g s) = ennreal.of_real (∫ (y : α) in s, (g - f) y ∂μ)
theorem
volume_region_between_eq_integral
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f g : α → ℝ}
{s : set α}
[measure_theory.sigma_finite μ]
(f_int : measure_theory.integrable_on f s μ)
(g_int : measure_theory.integrable_on g s μ)
(hs : measurable_set s)
(hfg : ∀ (x : α), x ∈ s → f x ≤ g x) :
⇑(μ.prod measure_theory.measure_space.volume) (region_between f g s) = ennreal.of_real (∫ (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.
theorem
real.integrable_of_summable_norm_Icc
{E : Type u_1}
[normed_add_comm_group E]
{f : C(ℝ, E)}
(hf : summable (λ (n : ℤ), ‖continuous_map.restrict (set.Icc 0 1) (f.comp (continuous_map.add_right ↑n))‖)) :
If the sequence with n-th term the the sup norm of λ 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 interval_integral). For the case
of finite integrals, see interval_integral.integral_comp_neg.