Theorems · Theorem · real analysis
AntitoneOn.integral_le_tsum_comp_add
∀ {f : ℝ → ℝ} (N : ℕ),
AntitoneOn f (Set.Ici ↑N) →
(Summable fun n => f ↑n) → (∀ t ∈ Set.Ioi ↑N, 0 ≤ f t) → ∫ (x : ℝ) in Set.Ioi ↑N, f x ≤ ∑' (n : ℕ), f ↑(n + N)The sum of a nonnegative, antitone function is bounded below by its integral.
- Defined in
- Mathlib.Analysis.SumIntegralComparisons
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 261 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites32
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Realstatement and proof · cited by 25,697
- NormedAddCommGroupproof · cited by 15,752
- NormedSpaceproof · cited by 12,499
- MeasureTheory.Measureproof · cited by 10,939
- nhdsproof · cited by 5,554
- Finset.sumproof · cited by 5,195
- Filter.Tendstoproof · cited by 3,814
- Filter.atTopproof · cited by 2,405
- SummationFilter.unconditionalstatement and proof · cited by 2,068
- MeasureTheory.integralstatement · cited by 1,779
- Filter.univ_mem'proof · cited by 1,672
Cited by1
Results whose statement or proof uses this declaration.
- AntitoneOn.integral_le_tsumproof · cited by 0