theorem
darbouxIntegral_add
{a b c : ℝ}
{f : ℝ → ℝ}
(hab : a < b)
(hbc : b < c)
(hbound : ∃ (M : ℝ), ∀ x ∈ Set.Icc a c, |f x| ≤ M)
:
lowerDarbouxIntegral f a c = lowerDarbouxIntegral f a b + lowerDarbouxIntegral f b c ∧ upperDarbouxIntegral f a c = upperDarbouxIntegral f a b + upperDarbouxIntegral f b c
Lemma 5.2.1: If a < b < c and f : [a, c] → ℝ is bounded, then the
lower and upper Darboux integrals over [a, c] split as the sums of the
integrals over [a, b] and [b, c]. That is,
∫̲_a^c f = ∫̲_a^b f + ∫̲_b^c f and ∫̅_a^c f = ∫̅_a^b f + ∫̅_b^c f.
Proposition 5.2.2: For a < b < c, a function f : [a, c] → ℝ is Riemann
integrable exactly when it is Riemann integrable on both [a, b] and [b, c].
If f is integrable on [a, c], then the integral splits as
∫_a^c f = ∫_a^b f + ∫_b^c f.
theorem
riemannIntegral_split
{a b c : ℝ}
{f : ℝ → ℝ}
(hab : a < b)
(hbc : b < c)
(hf : RiemannIntegrableOn f a c)
:
∃ (hf_ab : RiemannIntegrableOn f a b) (hf_bc : RiemannIntegrableOn f b c),
riemannIntegral f a c hf = riemannIntegral f a b hf_ab + riemannIntegral f b c hf_bc
theorem
riemannIntegrableOn_subinterval
{a b c d : ℝ}
{f : ℝ → ℝ}
(hf : RiemannIntegrableOn f a b)
(hac : a ≤ c)
(hcd : c ≤ d)
(hdb : d ≤ b)
:
RiemannIntegrableOn f c d
Corollary 5.2.3: If f ∈ ℛ([a, b]) and [c, d] ⊆ [a, b], then the
restriction of f to [c, d] belongs to ℛ([c, d]).