theorem Integration.integral_comparison_and_triangle (f g : ℝ → ℝ) (a b : ℝ) (hab : a ≤ b) (hf : ContinuousOn f (Set.Icc a b)) (hg : ContinuousOn g (Set.Icc a b)) : ((∀ x ∈ Set.Icc a b, f x ≤ g x) → ∫ (x : ℝ) in a..b, f x ≤ ∫ (x : ℝ) in a..b, g x) ∧ |∫ (x : ℝ) in a..b, f x| ≤ ∫ (x : ℝ) in a..b, |f x|

Comparison and triangle inequalities for the Riemann integral.

For continuous functions f, g : ℝ → ℝ on [a, b] with a ≤ b:

1. (Comparison) If f x ≤ g x for all x ∈ [a, b], then ∫ x in a..b, f x ≤ ∫ x in a..b, g x.
2. (Triangle inequality) |∫ x in a..b, f x| ≤ ∫ x in a..b, |f x|.

theorem Integration.integral_bounds (f : ℝ → ℝ) (a b : ℝ) (hab : a ≤ b) (hf : ContinuousOn f (Set.Icc a b)) : sInf (f '' Set.Icc a b) * (b - a) ≤ ∫ (x : ℝ) in a..b, f x ∧ ∫ (x : ℝ) in a..b, f x ≤ sSup (f '' Set.Icc a b) * (b - a)

Lower and upper bounds for the Riemann integral via the infimum and supremum.

If f : ℝ → ℝ is continuous on [a, b] with a ≤ b, then setting m_f = sInf (f '' [a, b]) and M_f = sSup (f '' [a, b]), we have m_f * (b - a) ≤ ∫ x in a..b, f x ≤ M_f * (b - a).

theorem Integration.integral_additivity (f : ℝ → ℝ) (a b c : ℝ) (hac : a < c) (hcb : c < b) (hf : ContinuousOn f (Set.Icc a b)) : ∫ (x : ℝ) in a..b, f x = (∫ (x : ℝ) in a..c, f x) + ∫ (x : ℝ) in c..b, f x

Additivity of the Riemann integral over adjacent intervals.

If f : ℝ → ℝ is continuous on [a, b] and a < c < b, then ∫ x in a..b, f x = (∫ x in a..c, f x) + ∫ x in c..b, f x.

theorem Integration.integral_linearity (f g : ℝ → ℝ) (a b α : ℝ) (hf : ContinuousOn f (Set.Icc a b)) (hg : ContinuousOn g (Set.Icc a b)) (hab : a ≤ b) : ∫ (x : ℝ) in a..b, α * f x + g x = (α * ∫ (x : ℝ) in a..b, f x) + ∫ (x : ℝ) in a..b, g x

Linearity of the Riemann integral.

If f, g : ℝ → ℝ are continuous on [a, b] with a ≤ b and α : ℝ, then ∫ x in a..b, (α * f x + g x) = α * (∫ x in a..b, f x) + ∫ x in a..b, g x.