Theorems · Theorem · real analysis

AntitoneOn.tsum_comp_add_le_integral

∀ {f : ℝ → ℝ} (N : ℕ),
  AntitoneOn f (Set.Ici ↑N) →
    MeasureTheory.IntegrableOn f (Set.Ioi ↑N) MeasureTheory.volume →
      (∀ t ∈ Set.Ioi ↑N, 0 ≤ f t) → ∑' (n : ℕ), f ↑(n + N + 1) ≤ ∫ (x : ℝ) in Set.Ioi ↑N, f x

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

Cites28

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
Finsetproof · cited by 13,712
Finset.sumproof · cited by 5,195
SummationFilter.unconditionalstatement · cited by 2,068
MeasureTheory.integralstatement · cited by 1,779
Filter.univ_mem'proof · cited by 1,672
MeasureTheory.Measure.restrictstatement · cited by 1,646
Filter.mp_memproof · cited by 1,537
Set.Ioistatement and proof · cited by 1,463
Finset.rangeproof · cited by 1,341
MeasureTheory.MeasureSpace.volumestatement and proof · cited by 1,323

Cited by2

Results whose statement or proof uses this declaration.

AntitoneOn.abs_tsum_sub_sum_range_le_integralproof · cited by 0
AntitoneOn.tsum_add_one_le_integralproof · cited by 0