Theorems · Theorem · real analysis
AntitoneOn.integrableOn_Ioi_zero_of_summable
∀ {f : ℝ → ℝ},
AntitoneOn f (Set.Ici 0) →
(Summable fun n => f ↑n) →
(∀ t ∈ Set.Ioi 0, 0 ≤ f t) → MeasureTheory.IntegrableOn f (Set.Ioi 0) MeasureTheory.volumeConverse to the integral test: a nonnegative, integrable, summable function is integrable.
- Defined in
- Mathlib.Analysis.SumIntegralComparisons
- Cited by
- 0 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.
Cites11
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
- SummationFilter.unconditionalstatement and proof · cited by 2,068
- Nat.cast_zeroproof · cited by 1,870
- Set.Ioistatement and proof · cited by 1,463
- MeasureTheory.MeasureSpace.volumestatement and proof · cited by 1,323
- Set.Icistatement and proof · cited by 1,070
- Summablestatement and proof · cited by 778
- MeasureTheory.IntegrableOnstatement and proof · cited by 548
- AntitoneOnstatement and proof · cited by 266
- AntitoneOn.integrableOn_Ioi_of_summable_comp_addproof · cited by 2
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.