Numerical series

TheoremGeometric series#

Mathlib states this as tsum_geometric_of_norm_lt_one.

tsum_geometric_of_norm_lt_one.{u_4} {K : Type u_4} [NormedDivisionRing K] {ξ : K} (h : ‖ξ‖ < 1) :
  ∑' (n : ℕ), ξ ^ n = (1 - ξ)⁻¹

Sources

• Mathlib documentation: tsum_geometric_of_norm_lt_one
• Source of tsum_geometric_of_norm_lt_one in Mathlib/Analysis/SpecificLimits/Normed.lean
• Mathlib undergraduate list: Single Variable Real Analysis › Numerical series

Mathlibtsum_geometric_of_norm_lt_one

Uses 6 · Used by 1

Statement usesInfinite sum · Metric space

Proof usesCompleteness of R · Hausdorff space · Order topology · Topological ring

Used byLiouville's theorem on existence of transcendental numbers

TheoremConvergence of \(p\)-series for \(p>1\)#

Test for convergence of the p-series: the real-valued series ∑' n : ℕ, 1 / n ^ p converges if and only if 1 < p.

Real.summable_one_div_nat_rpow {p : ℝ} : (Summable fun n => 1 / ↑n ^ p) ↔ 1 < p

Sources

• Mathlib documentation: Real.summable_one_div_nat_rpow
• Source of Real.summable_one_div_nat_rpow in Mathlib/Analysis/PSeries.lean
• Mathlib undergraduate list: Single Variable Real Analysis › Numerical series

MathlibReal.summable_one_div_nat_rpow

Uses 10

Statement usesBornology · Infinite sum · Order

Proof usesCharacteristic zero · Continuous function · Field \(\R\) of real numbers · Metric space · Module · Order topology · Ordered ring

TheoremComparison of a series and an integral#

Integral test: bounds the sum of a nonnegative antitone function by an integral.

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

Sources

• Mathlib documentation: AntitoneOn.tsum_le_integral
• Source of AntitoneOn.tsum_le_integral in Mathlib/Analysis/SumIntegralComparisons.lean
• Mathlib undergraduate list: Single Variable Real Analysis › Numerical series

MathlibAntitoneOn.tsum_le_integral

Uses 11

Statement usesBochner integral · Carathéodory's theorem (measure theory) · Lebesgue measure (Measures and integral calculus)

Proof usesCharacteristic p · Characteristic zero · Compactness in terms of filters · Completeness of R · Hausdorff space · Measurable function · Metric structure · Order topology

TheoremAlternating series#

The alternating series test for antitone sequences.

Antitone.tendsto_alternating_series_of_tendsto_zero {f : ℕ → ℝ} (hfa : Antitone f)
  (hf0 : Filter.Tendsto f Filter.atTop (nhds 0)) :
  ∃ l, Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i) Filter.atTop (nhds l)

Sources

• Mathlib documentation: Antitone.tendsto_alternating_series_of_tendsto_zero
• Source of Antitone.tendsto_alternating_series_of_tendsto_zero in Mathlib/Analysis/SpecificLimits/Normed.lean
• Mathlib undergraduate list: Single Variable Real Analysis › Numerical series

MathlibAntitone.tendsto_alternating_series_of_tendsto_zero

Uses 8 · Used by 1

Statement usesBornology · Finite set · Order

Proof usesCompleteness of R · Normed vector space over a normed field · Topological ring · Topology on a normed vector space · Uniformly continuous function

Used byLeibniz’s Series for Pi

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.