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