theorem riemannIntegral_linearity {a b α : ℝ} {f g : ℝ → ℝ} (hf : RiemannIntegrableOn f a b) (hg : RiemannIntegrableOn g a b) : (∃ (hαf : RiemannIntegrableOn (fun (x : ℝ) => α * f x) a b), riemannIntegral (fun (x : ℝ) => α * f x) a b hαf = α * riemannIntegral f a b hf) ∧ ∃ (hfg : RiemannIntegrableOn (fun (x : ℝ) => f x + g x) a b), riemannIntegral (fun (x : ℝ) => f x + g x) a b hfg = riemannIntegral f a b hf + riemannIntegral g a b hg

Proposition 5.2.4 (Linearity): Let f and g be Riemann integrable on the closed interval [a, b] and let α : ℝ.

• (i) The scalar multiple α • f belongs to ℛ([a, b]) and ∫_a^b α • f = α * ∫_a^b f.
• (ii) The sum f + g belongs to ℛ([a, b]) and ∫_a^b (f + g) = ∫_a^b f + ∫_a^b g.

theorem darbouxIntegral_add_le_add {a b : ℝ} {f g : ℝ → ℝ} (hbound_f : ∃ (M : ℝ), ∀ x ∈ Set.Icc a b, |f x| ≤ M) (hbound_g : ∃ (M : ℝ), ∀ x ∈ Set.Icc a b, |g x| ≤ M) : upperDarbouxIntegral (fun (x : ℝ) => f x + g x) a b ≤ upperDarbouxIntegral f a b + upperDarbouxIntegral g a b ∧ lowerDarbouxIntegral (fun (x : ℝ) => f x + g x) a b ≥ lowerDarbouxIntegral f a b + lowerDarbouxIntegral g a b

Proposition 5.2.5: Let bounded functions f, g : [a, b] → ℝ. Then the upper Darboux integral of their sum is at most the sum of their upper Darboux integrals, and the lower Darboux integral of their sum is at least the sum of their lower Darboux integrals.

theorem darbouxIntegral_monotone {a b : ℝ} {f g : ℝ → ℝ} (hbound_f : ∃ (M : ℝ), ∀ x ∈ Set.Icc a b, |f x| ≤ M) (hbound_g : ∃ (M : ℝ), ∀ x ∈ Set.Icc a b, |g x| ≤ M) (hmono : ∀ x ∈ Set.Icc a b, f x ≤ g x) : lowerDarbouxIntegral f a b ≤ lowerDarbouxIntegral g a b ∧ upperDarbouxIntegral f a b ≤ upperDarbouxIntegral g a b

Proposition 5.2.6 (Monotonicity): If bounded functions f, g : [a, b] → ℝ satisfy f x ≤ g x on [a, b], then their lower and upper Darboux integrals obey ∫̲_a^b f ≤ ∫̲_a^b g and ∫̅_a^b f ≤ ∫̅_a^b g. Moreover, if f and g are Riemann integrable on [a, b], then ∫_a^b f ≤ ∫_a^b g.

theorem riemannIntegral_monotone {a b : ℝ} {f g : ℝ → ℝ} (hmono : ∀ x ∈ Set.Icc a b, f x ≤ g x) (hf : RiemannIntegrableOn f a b) (hg : RiemannIntegrableOn g a b) : riemannIntegral f a b hf ≤ riemannIntegral g a b hg