x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
⊢ (∫ (x : ℝ) in ↑a..↑b, -f x) ≤ ∑ x in Finset.Ico a b, -f ↑x
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
⊢ ∑ x in Finset.Ico a b, f ↑x ≤ ∫ (x : ℝ) in ↑a..↑b, f x
rw [← neg_le_neg_iff, ← Finset.sum_neg_distrib, ← intervalIntegral.integral_neg]
no goals
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
⊢ (∫ (x : ℝ) in ↑a..↑b, -f x) ≤ ∑ x in Finset.Ico a b, -f ↑x
exact hf.neg.integral_le_sum_Ico hab