Theorems · Theorem · sequences and series
ENNReal.tsum_schlomilch_le
∀ {u : ℕ → ℕ} {f : ℕ → ENNReal} {C : ℕ},
(∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m) →
(∀ (n : ℕ), 0 < u n) →
(∀ (n : ℕ), 0 ≤ f n) →
Monotone u →
SuccDiffBounded C u →
∑' (k : ℕ), (↑(u (k + 1)) - ↑(u k)) * f (u k) ≤ (↑(u 1) - ↑(u 0)) * f (u 0) + ↑C * ∑' (k : ℕ), f k- Defined in
- Mathlib.Analysis.PSeries
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 132 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites21
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- ENNRealstatement and proof · cited by 9,879
- Finset.sumproof · cited by 5,195
- Finset.sum_congrproof · cited by 2,323
- SummationFilter.unconditionalstatement and proof · cited by 2,068
- le_reflproof · cited by 2,061
- Monotonestatement and proof · cited by 1,397
- Finset.rangeproof · cited by 1,341
- tsumstatement and proof · cited by 1,148
- add_le_addproof · cited by 666
- le_imp_le_of_le_of_leproof · cited by 576
- Finset.Icoproof · cited by 450
- nsmul_eq_mulproof · cited by 369
Cited by1
Results whose statement or proof uses this declaration.
- NNReal.summable_schlomilch_iffproof · cited by 2