Real.integrable_of_summable_norm_Icc
theorem Real.integrable_of_summable_norm_Icc :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : C(ℝ, E)},
(Summable fun n => ‖ContinuousMap.restrict (Set.Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))‖) →
MeasureTheory.Integrable (⇑f) MeasureTheory.volume
The theorem states that if we have a sequence whose `n`-th term is the supremum norm of the function `f` shifted by `n` on the interval from 0 to 1, and if this sequence is summable, then `f` is integrable over the real numbers. More formally, let `E` be a normed additive commutative group and `f` be a continuous function from the real numbers to `E`. If the supremum norm of the function obtained by restricting `f` composed with the continuous map `fun x => x + n` to the closed interval from 0 to 1 is summable over all integers `n`, then `f` is integrable with respect to the Lebesgue measure on the real numbers.
More concisely: If the sequence of supremum norms of a continuous function's shifts over closed intervals is summable, then the function is integrable with respect to Lebesgue measure.
|
volume_regionBetween_eq_integral
theorem volume_regionBetween_eq_integral :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ℝ} {s : Set α}
[inst_1 : MeasureTheory.SigmaFinite μ],
MeasureTheory.IntegrableOn f s μ →
MeasureTheory.IntegrableOn g s μ →
MeasurableSet s →
(∀ x ∈ s, f x ≤ g x) →
↑↑(μ.prod MeasureTheory.volume) (regionBetween f g s) = ENNReal.ofReal (∫ (y : α) in s, (g - f) y ∂μ)
This theorem states that for any given measurable space 'α' and measure 'μ', if there are two functions 'f' and 'g' defined on a set 's' in 'α', and if both 'f' and 'g' are integrable on 's' with respect to the measure 'μ', and furthermore, if for every 'x' in 's', 'f(x)' is less than or equal to 'g(x)', then the volume of the region between the two functions 'f' and 'g' can be expressed as an integral. Specifically, the volume of the region between functions 'f' and 'g' is equal to the extended non-negative real number equivalent of the integral over 's' of '(g - f) y' with respect to the measure 'μ'.
More concisely: For measurable functions `f` and `g` on a measurable space `(α, μ)` with integrable differences on a set `s`, the volume of the region between `f` and `g` on `s` equals the integral of `(g - f) dμ`.
|