Properties of integration with respect to the Lebesgue measure #
theorem
volume_regionBetween_eq_integral'
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{f g : α → Real}
{s : Set α}
[MeasureTheory.SigmaFinite μ]
(f_int : MeasureTheory.IntegrableOn f s μ)
(g_int : MeasureTheory.IntegrableOn g s μ)
(hs : MeasurableSet s)
(hfg : (MeasureTheory.ae (μ.restrict s)).EventuallyLE f g)
:
Eq (DFunLike.coe (μ.prod MeasureTheory.MeasureSpace.volume) (regionBetween f g s))
(ENNReal.ofReal (MeasureTheory.integral (μ.restrict s) fun (y : α) => HSub.hSub g f y))
theorem
volume_regionBetween_eq_integral
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{f g : α → Real}
{s : Set α}
[MeasureTheory.SigmaFinite μ]
(f_int : MeasureTheory.IntegrableOn f s μ)
(g_int : MeasureTheory.IntegrableOn g s μ)
(hs : MeasurableSet s)
(hfg : ∀ (x : α), Membership.mem s x → LE.le (f x) (g x))
:
Eq (DFunLike.coe (μ.prod MeasureTheory.MeasureSpace.volume) (regionBetween f g s))
(ENNReal.ofReal (MeasureTheory.integral (μ.restrict s) fun (y : α) => HSub.hSub 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}
[NormedAddCommGroup E]
{f : ContinuousMap Real E}
(hf :
Summable fun (n : Int) => Norm.norm (ContinuousMap.restrict (Set.Icc 0 1) (f.comp (ContinuousMap.addRight n.cast))))
:
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.
theorem
integral_comp_neg_Iic
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace Real E]
(c : Real)
(f : Real → E)
:
Eq (MeasureTheory.integral (MeasureTheory.MeasureSpace.volume.restrict (Set.Iic c)) fun (x : Real) => f (Neg.neg x))
(MeasureTheory.integral (MeasureTheory.MeasureSpace.volume.restrict (Set.Ioi (Neg.neg c))) fun (x : Real) => f x)
theorem
integral_comp_neg_Ioi
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace Real E]
(c : Real)
(f : Real → E)
:
Eq (MeasureTheory.integral (MeasureTheory.MeasureSpace.volume.restrict (Set.Ioi c)) fun (x : Real) => f (Neg.neg x))
(MeasureTheory.integral (MeasureTheory.MeasureSpace.volume.restrict (Set.Iic (Neg.neg c))) fun (x : Real) => f x)
theorem
integral_comp_abs
{f : Real → Real}
:
Eq (MeasureTheory.integral MeasureTheory.MeasureSpace.volume fun (x : Real) => f (abs x))
(HMul.hMul 2 (MeasureTheory.integral (MeasureTheory.MeasureSpace.volume.restrict (Set.Ioi 0)) fun (x : Real) => f x))