Theorems · Theorem · real analysis

AntitoneOn.sum_Ico_le_integral

∀ {f : ℝ → ℝ} {a b : ℕ},
  AntitoneOn f (Set.Icc ↑a ↑b) →
    MeasureTheory.IntegrableOn f (Set.Ioi ↑a) MeasureTheory.volume →
      (∀ t ∈ Set.Ioi ↑a, 0 ≤ f t) → ∑ n ∈ Finset.Ico a b, f ↑(n + 1) ≤ ∫ (x : ℝ) in Set.Ioi ↑a, f x

The partial sums of a nonnegative antitone function are bounded by the integral over (a, ∞).

Defined in: Mathlib.Analysis.SumIntegralComparisons
Cited by: 3 results in Mathlib
Foundations: Depth 261 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.

Cites26

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
Finset.sumstatement · cited by 5,195
Nat.cast_oneproof · cited by 2,501
Finset.sum_congrproof · cited by 2,323
LT.lt.leproof · cited by 2,189
le_reflproof · cited by 2,061
MeasureTheory.integralstatement and proof · cited by 1,779
Set.Iccstatement and proof · cited by 1,702
MeasureTheory.Measure.restrictstatement and proof · cited by 1,646
Set.Ioistatement and proof · cited by 1,463
MeasureTheory.MeasureSpace.volumestatement and proof · cited by 1,323

Cited by3

Results whose statement or proof uses this declaration.

AntitoneOn.tsum_comp_add_le_integralproof · cited by 2
AntitoneOn.summable_of_integrableOn_Ioiproof · cited by 2
AntitoneOn.sum_range_le_integralproof · cited by 0