Theorems · Theorem · real analysis
integral_le_sum_mul_Ico_of_antitone_monotone
∀ {a b : ℕ} {f g : ℝ → ℝ},
a ≤ b →
AntitoneOn f (Set.Icc ↑a ↑b) →
MonotoneOn g (Set.Icc (↑a - 1) (↑b - 1)) →
0 ≤ f ↑b → 0 ≤ g (↑a - 1) → ∫ (x : ℝ) in ↑a..↑b, f x * g (x - 1) ≤ ∑ i ∈ Finset.Ico a b, f ↑i * g ↑i- Defined in
- Mathlib.Analysis.SumIntegralComparisons
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 260 from the axioms · uses propext, Classical.choice, Quot.sound
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 by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.