Theorems 58 to 78

TheoremFormula for the Number of Combinations #

Mathlib records this with 2 declarations.

Finset.card_powersetCard: Formula for the Number of Combinations

Finset.card_powersetCard.{u_1} {α : Type u_1} (n : ℕ) (s : Finset α) :
  (Finset.powersetCard n s).card = s.card.choose n

Finset.mem_powersetCard.

Finset.mem_powersetCard.{u_1} {α : Type u_1} {n : ℕ} {s t : Finset α} :
  s ∈ Finset.powersetCard n t ↔ s ⊆ t ∧ s.card = n

Sources

MathlibFinset.card_powersetCard · Finset.mem_powersetCard

Uses 2 · Used by 5

Statement usesFinite set · Natural number

Used byAhlswede-Zhang identity · LYM inequality · Sauer-Shelah lemma · Erdős–Ko–Rado theorem · Newton's identities

59. The Laws of Large Numbers

TheoremBezout’s Theorem #

Bézout's lemma: given x y : ℕ, gcd x y = x * a + y * b, where a = gcd_a x y and b = gcd_b x y are computed by the extended Euclidean algorithm.

Nat.gcd_eq_gcd_ab (x y : ℕ) : ↑(x.gcd y) = ↑x * x.gcdA y + ↑y * x.gcdB y

Sources

MathlibNat.gcd_eq_gcd_ab

Uses 1 · Used by 2

Statement usesEuclid's' algorithm

Used byDirichlet’s Theorem · Mahler's theorem

TheoremTheorem of Ceva #

Ceva's theorem for a triangle, expressed using division of distances.

Affine.Triangle.prod_dist_div_dist_eq_one_of_mem_line_of_mem_line.{u_1, u_2, u_3} {𝕜 : Type u_1}
  {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [NormedField 𝕜] [NormedSpace 𝕜 V]
  [MetricSpace P] [NormedAddTorsor V P] {t : Affine.Triangle 𝕜 P} {p : Fin 3 → P} {p' : P}
  (hp0 : ∀ (i : Fin 3), p i ≠ t.points (i + 2))
  (hp : ∀ (i : Fin 3), p i ∈ line[𝕜, t.points (i + 1), t.points (i + 2)])
  (hp' : ∀ (i : Fin 3), p' ∈ line[𝕜, t.points i, p i]) :
  ∏ i, dist (t.points (i + 1)) (p i) / dist (p i) (t.points (i + 2)) = 1

Sources

MathlibAffine.Triangle.prod_dist_div_dist_eq_one_of_mem_line_of_mem_line

Uses 7

Statement usesAffine span · Euclidean affine space · Finite set · Linear map · Normed vector space over a normed field

Proof usesAffine function · Field $\R$ of real numbers

62. Fair Games Theorem

TheoremCantor’s Theorem #

Cantor's diagonal argument implies that there are no surjective functions from α to Set α.

Function.cantor_surjective.{u_4} {α : Type u_4} (f : α → Set α) : ¬Function.Surjective f

Sources

MathlibFunction.cantor_surjective

Uses 1 · Used by 1

Statement usesSet

Used bySmall category

TheoremL’Hopital’s Rule #

L'Hôpital's rule for approaching a real, deriv version

deriv.lhopital_zero_nhds {a : ℝ} {l : Filter ℝ} {f g : ℝ → ℝ}
  (hdf : ∀ᶠ (x : ℝ) in nhds a, DifferentiableAt ℝ f x) (hg' : ∀ᶠ (x : ℝ) in nhds a, deriv g x ≠ 0)
  (hfa : Filter.Tendsto f (nhds a) (nhds 0)) (hga : Filter.Tendsto g (nhds a) (nhds 0))
  (hdiv : Filter.Tendsto (fun x => deriv f x / deriv g x) (nhds a) l) :
  Filter.Tendsto (fun x => f x / g x) (nhdsWithin a {a}ᶜ) l

Sources

Mathlibderiv.lhopital_zero_nhds

Uses 13

Statement usesDifferentiable function between normed vector spaces · Differentials (linear tangent functions)

Proof usesAssociative algebra over a commutative ring · Closure · Completeness · Convex subsets · Derivative at a point · Field $\R$ of real numbers · Finite set · Normed vector space over a normed field · Ordered ring · Squeeze theorem · Topological ring

TheoremIsosceles Triangle Theorem #

Isosceles Triangle Theorem: Pons asinorum, angle-at-point form.

EuclideanGeometry.angle_eq_angle_of_dist_eq.{u_1, u_2} {V : Type u_1} {P : Type u_2}
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P]
  {p₁ p₂ p₃ : P} (h : dist p₁ p₂ = dist p₁ p₃) :
  EuclideanGeometry.angle p₁ p₂ p₃ = EuclideanGeometry.angle p₁ p₃ p₂

Sources

MathlibEuclideanGeometry.angle_eq_angle_of_dist_eq

Uses 2

Statement usesAngle · Euclidean affine space

TheoremSum of a Geometric Series #

Mathlib records this with 2 declarations.

geom_sum_Ico.

geom_sum_Ico.{u_1} {K : Type u_1} [DivisionRing K] {x : K} (hx : x ≠ 1) {m n : ℕ} (hmn : m ≤ n) :
  ∑ i ∈ Finset.Ico m n, x ^ i = (x ^ n - x ^ m) / (x - 1)

NNReal.hasSum_geometric: Sum of a Geometric Series

NNReal.hasSum_geometric {r : NNReal} (hr : r < 1) : HasSum (fun n => r ^ n) (1 - r)⁻¹

Sources

Mathlibgeom_sum_Ico · NNReal.hasSum_geometric

Uses 9 · Used by 3

Statement usesInfinite sum · Real number

Proof usesBornology · Closure · Field $\R$ of real numbers · Order · Order topology · Ordered ring · Topological ring

Used byBaire theorem · Contraction mapping theorem · Egorov's theorem

TheoremSum of an arithmetic series #

Gauss' summation formula

Finset.sum_range_id (n : ℕ) : ∑ i ∈ Finset.range n, i = n * (n - 1) / 2

Sources

MathlibFinset.sum_range_id

Uses 2

Statement usesFinite set · Natural number

DefinitionGreatest Common Divisor Algorithm #

Mathlib records this with 3 declarations.

EuclideanDomain.gcd: gcd a b is a (non-unique) element such that gcd a b ∣ a gcd a b ∣ b, and for any element c such that c ∣ a and c ∣ b, then c ∣ gcd a b

EuclideanDomain.gcd.{u} {R : Type u} [EuclideanDomain R] [DecidableEq R] (a b : R) : R

EuclideanDomain.gcd_dvd.

EuclideanDomain.gcd_dvd.{u} {R : Type u} [EuclideanDomain R] [DecidableEq R] (a b : R) :
  EuclideanDomain.gcd a b ∣ a ∧ EuclideanDomain.gcd a b ∣ b

EuclideanDomain.dvd_gcd.

EuclideanDomain.dvd_gcd.{u} {R : Type u} [EuclideanDomain R] [DecidableEq R] {a b c : R} :
  c ∣ a → c ∣ b → c ∣ EuclideanDomain.gcd a b

Sources

MathlibEuclideanDomain.gcd · EuclideanDomain.gcd_dvd · EuclideanDomain.dvd_gcd

Uses 2 · Used by 1

Statement usesEuclidean domain · Integer

Used byPrimitive element theorem

TheoremThe Perfect Number Theorem #

Perfect Number Theorem: Euler's theorem that even perfect numbers can be factored as a power of two times a Mersenne prime.

Theorems100.Nat.eq_two_pow_mul_prime_mersenne_of_even_perfect {n : ℕ} (ev : Even n)
  (perf : n.Perfect) : ∃ k, Nat.Prime (mersenne (k + 1)) ∧ n = 2 ^ k * mersenne (k + 1)

Sources

MathlibTheorems100.Nat.eq_two_pow_mul_prime_mersenne_of_even_perfect

Uses 5

Statement usesFinite set · Irreducible element · Natural number

Proof usesArithmetic functions · Ordered ring

TheoremAscending or Descending Sequences (Erdős–Szekeres Theorem)#

Erdős–Szekeres Theorem: Given a sequence of more than r * s distinct values, there is an increasing sequence of length longer than r or a decreasing sequence of length longer than s.

Proof idea: We label each value in the sequence with two numbers specifying the longest increasing subsequence ending there, and the longest decreasing subsequence ending there. We then show the pair of labels must be unique. Now if there is no increasing sequence longer than r and no decreasing sequence longer than s, then there are at most r * s possible labels, which is a contradiction if there are more than r * s elements.

Theorems100.erdos_szekeres.{u_1, u_2} {α : Type u_1} {β : Type u_2} [Fintype α] [LinearOrder α]
  [LinearOrder β] {r s : ℕ} {f : α → β} (hn : r * s < Fintype.card α) (hf : Function.Injective f) :
  (∃ t, r < t.card ∧ StrictMonoOn f ↑t) ∨ ∃ t, s < t.card ∧ StrictAntiOn f ↑t

Sources

MathlibTheorems100.erdos_szekeres

Uses 2

Statement usesFinite set · Natural number

74. The Principle of Mathematical Induction

TheoremThe Mean Value Theorem (Freek Wiedijk's 100 theorems)#

Lagrange's Mean Value Theorem, deriv version.

exists_deriv_eq_slope (f : ℝ → ℝ) {a b : ℝ} (hab : a < b) (hfc : ContinuousOn f (Set.Icc a b))
  (hfd : DifferentiableOn ℝ f (Set.Ioo a b)) : ∃ c ∈ Set.Ioo a b, deriv f c = (f b - f a) / (b - a)

The 1000+ list (Q189136) also cites exists_ratio_deriv_eq_ratio_slope.

Sources

Mathlibexists_deriv_eq_slope

Uses 10 · Used by 2

Statement usesDifferentials (linear tangent functions) · Holomorphic functions

Proof usesAssociative algebra over a commutative ring · Completeness · Derivative at a point · Differentiable function between normed vector spaces · Field $\R$ of real numbers · Finite set · Normed vector space over a normed field · Topological ring

Used byCharacterization of convexity · Liouville's theorem on existence of transcendental numbers

DefinitionFourier Series #

Mathlib records this with 2 declarations.

fourierCoeff: The n-th Fourier coefficient of a function AddCircle T → E, for E a complete normed ℂ-vector space, defined as the integral over AddCircle T of fourier (-n) t • f t.

fourierCoeff.{u_1} {T : ℝ} [hT : Fact (0 < T)] {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℂ E] (f : AddCircle T → E) (n : ℤ) : E

hasSum_fourier_series_L2: The Fourier series of an L2 function f sums to f, in the L² space of AddCircle T.

hasSum_fourier_series_L2 {T : ℝ} [hT : Fact (0 < T)]
  (f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)) :
  HasSum (fun i => fourierCoeff (↑↑f) i • fourierLp 2 i) f

Sources

MathlibfourierCoeff · hasSum_fourier_series_L2

Uses 17 · Used by 3

Statement usesBochner integral · Borel sigma-algebra · Carathéodory's theorem (measure theory) · Compact open topology · Cos (extension of trigonometric functions to the complex plane) · Field $\C$ of complex numbers · Homeomorphisms · Inner product space, over $R$ or $C$ · Lipschitz continuity · Topological ring

Proof usesCompleteness of $L^2$ · Completeness of $l^2$ · Example, the Hilbert basis of trigonometric polynomials · Heine-Borel theorem (finite-dimensional normed spaces are proper) · Probability measure · Urysohn's lemma · Weierstrass trigonometric approximation theorem

Used byEuler’s Summation of 1 + (1/2)^2 + (1/3)^2 + …. · Parseval formula for Fourier series · Poisson’s formula

TheoremSum of kth powers #

Mathlib records this with 2 declarations.

sum_range_pow: Faulhaber's theorem relating the sum of p-th powers to the Bernoulli numbers: $$\sum_{k=0}^{n-1} k^p = \sum_{i=0}^p B_i\binom{p+1}{i}\frac{n^{p+1-i}}{p+1}.$$ See https://proofwiki.org/wiki/Faulhaber%27s_Formula and [orosi2018faulhaber] for the proof provided here.

sum_range_pow (n p : ℕ) :
  ∑ k ∈ Finset.range n, ↑k ^ p =
    ∑ i ∈ Finset.range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / (↑p + 1)

sum_Ico_pow: Alternate form of Faulhaber's theorem, relating the sum of p-th powers to the Bernoulli numbers: $$\sum_{k=1}^{n} k^p = \sum_{i=0}^p (-1)^iB_i\binom{p+1}{i}\frac{n^{p+1-i}}{p+1}.$$ Deduced from sum_range_pow.

sum_Ico_pow (n p : ℕ) :
  ∑ k ∈ Finset.Ico 1 (n + 1), ↑k ^ p =
    ∑ i ∈ Finset.range (p + 1), bernoulli' i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / (↑p + 1)

Sources

Mathlibsum_range_pow · sum_Ico_pow

Uses 10 · Used by 1

Statement usesBernoulli numbers

Proof usesAssociative algebra over a commutative ring · Characteristic p · Characteristic zero · Euclidean domain · Field $\Q$ of rational numbers · Linear map · Metric space · Ordered ring · The Binomial Theorem

Used byVon Staudt–Clausen theorem

78. The Cauchy-Schwarz Inequality

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

Theorems 58 to 78

TheoremFormula for the Number of Combinations#

Sources

TheoremBezout’s Theorem#

Sources

TheoremTheorem of Ceva#

Sources

TheoremCantor’s Theorem#

Sources

TheoremL’Hopital’s Rule#

Sources

TheoremIsosceles Triangle Theorem#

Sources

TheoremSum of a Geometric Series#

Sources

TheoremSum of an arithmetic series#

Sources

DefinitionGreatest Common Divisor Algorithm#

Sources

TheoremThe Perfect Number Theorem#

Sources

TheoremAscending or Descending Sequences (Erdős–Szekeres Theorem)#

Sources

TheoremThe Mean Value Theorem (Freek Wiedijk's 100 theorems)#

Sources

DefinitionFourier Series#

Sources

TheoremSum of kth powers#

Sources

TheoremFormula for the Number of Combinations #

TheoremBezout’s Theorem #

TheoremTheorem of Ceva #

TheoremCantor’s Theorem #

TheoremL’Hopital’s Rule #

TheoremIsosceles Triangle Theorem #

TheoremSum of a Geometric Series #

TheoremSum of an arithmetic series #

DefinitionGreatest Common Divisor Algorithm #

TheoremThe Perfect Number Theorem #

DefinitionFourier Series #

TheoremSum of kth powers #