theorem sum_le_integral_of_le {a b : ℕ} {f g : ℝ → ℝ} (hab : a ≤ b) (h : ∀ i ∈ Set.Ico a b, ∀ x ∈ Set.Ico ↑i ↑(i + 1), f ↑i ≤ g x) (hg : MeasureTheory.IntegrableOn g (Set.Ico ↑a ↑b) MeasureTheory.volume) : ∑ i ∈ Finset.Ico a b, f ↑i ≤ ∫ (x : ℝ) in ↑a..↑b, g x

theorem sum_mul_le_integral_of_monotone_antitone {a b : ℕ} {f g : ℝ → ℝ} (hab : a ≤ b) (hf : MonotoneOn f (Set.Icc ↑a ↑b)) (hg : AntitoneOn g (Set.Icc (↑a - 1) (↑b - 1))) (fpos : 0 ≤ f ↑a) (gpos : 0 ≤ g (↑b - 1)) : ∑ i ∈ Finset.Ico a b, f ↑i * g ↑i ≤ ∫ (x : ℝ) in ↑a..↑b, f x * g (x - 1)