Theorems · Theorem · real analysis

sum_mul_Ico_le_integral_of_monotone_antitone

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

Defined in: Mathlib.Analysis.SumIntegralComparisons
Cited by: 1 results in Mathlib
Foundations: Depth 259 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites28

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement and proof · cited by 25,697
Finset.sumstatement · cited by 5,195
Nat.cast_oneproof · cited by 2,501
le_reflproof · cited by 2,061
Set.Iccstatement and proof · cited by 1,702
MeasureTheory.MeasureSpace.volumestatement and proof · cited by 1,323
Set.Icoproof · cited by 799
Nat.cast_addproof · cited by 586
le_imp_le_of_le_of_leproof · cited by 576
intervalIntegralstatement · cited by 546
Finset.Icostatement · cited by 450
Int.cast_natCastproof · cited by 393

Cited by1

Results whose statement or proof uses this declaration.

sum_Ico_pow_mul_exp_neg_leproof · cited by 1