Theorems 30 to 57

TheoremThe Ballot Problem#

The ballot problem.

Ballot.ballot_problem (q p : ℕ) :
  q < p →
    (ProbabilityTheory.uniformOn (Ballot.countedSequence p q)) Ballot.staysPositive =
      (↑p - ↑q) / (↑p + ↑q)
Sources
MathlibBallot.ballot_problem
Uses 9
Statement usesConditional probability · Counting measure
Proof usesCharacteristic p · Characteristic zero · Field \(\R\) of real numbers · Order · Ordered ring · Probability measure · Ring structure \(\Z\)

TheoremFermat’s Last Theorem#

Mathlib states this as FermatLastTheorem but does not prove it.

FermatLastTheorem : Prop

Formalized outside Mathlib; the 100 theorems list links the formalization.

External Lean proof of FermatLastTheorem, building on the Imperial College FLT project, flt-regular, and mathlib. The Imperial College FLT project is at https://imperialcollegelondon.github.io/FLT/.

The 1000+ list (Q132469): Formalisation of the proof is on-going in https://imperialcollegelondon.github.io/FLT/.

Sources

TheoremDivergence of the Harmonic Series#

Divergence of the Harmonic Series

Real.tendsto_sum_range_one_div_nat_succ_atTop :
  Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, 1 / (↑i + 1)) Filter.atTop Filter.atTop
Sources
MathlibReal.tendsto_sum_range_one_div_nat_succ_atTop
Uses 10
Statement usesFinite set · Real number
Proof usesCharacteristic zero · Continuous function · Field \(\R\) of real numbers · Infinite sum · Metric space · Module · Order topology · Ordered ring

TheoremThe Solution of a Cubic#

The Solution of Cubic. The roots of a cubic polynomial whose discriminant is nonzero.

Theorems100.cubic_eq_zero_iff.{u_1} {K : Type u_1} [Field K] (a b c d : K) {ω p q r s t : K}
  [Invertible 2] [Invertible 3] (ha : a ≠ 0) (hω : IsPrimitiveRoot ω 3)
  (hp : p = (3 * a * c - b ^ 2) / (9 * a ^ 2)) (hp_nonzero : p ≠ 0)
  (hq : q = (9 * a * b * c - 2 * b ^ 3 - 27 * a ^ 2 * d) / (54 * a ^ 3))
  (hr : r ^ 2 = q ^ 2 + p ^ 3) (hs3 : s ^ 3 = q + r) (ht : t * s = p) (x : K) :
  a * x ^ 3 + b * x ^ 2 + c * x + d = 0 ↔
    x = s - t - b / (3 * a) ∨
      x = s * ω - t * ω ^ 2 - b / (3 * a) ∨ x = s * ω ^ 2 - t * ω - b / (3 * a)
Sources
MathlibTheorems100.cubic_eq_zero_iff
Uses 6
Statement usesField · Invertible elements · Rational number
Proof usesCyclotomic polynomials in \(\Q[X]\) · Irreducible element · Local ring

TheoremArithmetic Mean/Geometric Mean#

AM-GM inequality: The geometric mean is less than or equal to the arithmetic mean, weighted version for real-valued nonnegative functions.

Real.geom_mean_le_arith_mean_weighted.{u} {ι : Type u} (s : Finset ι) (w z : ι → ℝ)
  (hw : ∀ i ∈ s, 0 ≤ w i) (hw' : ∑ i ∈ s, w i = 1) (hz : ∀ i ∈ s, 0 ≤ z i) :
  ∏ i ∈ s, z i ^ w i ≤ ∑ i ∈ s, w i * z i
Sources
MathlibReal.geom_mean_le_arith_mean_weighted
Uses 5 · Used by 1
Statement usesFinite set · Real number
Proof usesJensen's inequality (finite sum version) · Logarithm · Ordered ring
Used byHölder's inequality

TheoremSolutions to Pell’s Equation (Freek Wiedijk's 100 theorems)#

Mathlib records this with 2 declarations.

Pell.eq_pell: Every solution to Pell's equation is recursively obtained from the initial solution (1,0) using the recursion pell.

Pell.eq_pell {a : ℕ} (a1 : 1 < a) {x y : ℕ} (hp : x * x - (a * a - 1) * y * y = 1) :
  ∃ n, x = Pell.xn a1 n ∧ y = Pell.yn a1 n

Pell.exists_of_not_isSquare: If d is a positive integer that is not a square, then there is a nontrivial solution to the Pell equation x^2 - d*y^2 = 1.

Pell.exists_of_not_isSquare {d : ℤ} (h₀ : 0 < d) (hd : ¬IsSquare d) :
  ∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0

In pell.eq_pell, d is defined to be a*a - 1 for an arbitrary a > 1.

The 1000+ list (Q853067): In pell.eq_pell, d is defined to be a*a - 1 for an arbitrary a > 1.

Sources
MathlibPell.eq_pell · Pell.exists_of_not_isSquare
Uses 4 · Used by 1
Statement usesSolutions to Pell's equation (Number theory)
Proof usesDirichlet's approximation theorem · Euclidean domain · Field \(\Q\) of rational numbers
Used byMatiyasevič's theorem

TheoremMinkowski’s Fundamental Theorem#

The Minkowski Convex Body Theorem. If s is a convex symmetric domain of E whose volume is large enough compared to the covolume of a lattice L of E, then it contains a non-zero lattice point of L.

MeasureTheory.exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure.{u_1} {E : Type u_1}
  [MeasurableSpace E] {μ : MeasureTheory.Measure E} {F s : Set E} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [BorelSpace E] [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] {L : AddSubgroup E}
  [Countable ↥L] (fund : MeasureTheory.IsAddFundamentalDomain (↥L) F μ) (h_symm : ∀ x ∈ s, -x ∈ s)
  (h_conv : Convex ℝ s) (h : μ F * 2 ^ Module.finrank ℝ E < μ s) : ∃ x, x ≠ 0 ∧ ↑x ∈ s
Sources
MathlibMeasureTheory.exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure
Uses 15 · Used by 2
Statement usesAlmost sure convergence · Associative algebra over a commutative ring · Borel sigma-algebra · Carathéodory's theorem (measure theory) · Cardinal · Compactness in terms of filters · Convex subsets · Finite-dimensionality · Linear independence · Measurable function · Normed vector space over a normed field · Positive measure
Proof usesCharacteristic zero · Completeness of R · Continuous function
Used byDirichlet unit theorem · Finiteness of the class number

TheoremSum of the Reciprocals of the Triangular Numbers#

Sum of the Reciprocals of the Triangular Numbers

Theorems100.inverse_triangle_sum (n : ℕ) :
  ∑ k ∈ Finset.range n, 2 / (↑k * (↑k + 1)) = if n = 0 then 0 else 2 - 2 / ↑n
Sources
MathlibTheorems100.inverse_triangle_sum
Uses 5
Statement usesFinite set · Rational number
Proof usesCharacteristic zero · Field \(\Q\) of rational numbers · Ordered ring

TheoremThe Binomial Theorem#

The binomial theorem

add_pow.{u_1} {R : Type u_1} [CommSemiring R] (x y : R) (n : ℕ) :
  (x + y) ^ n = ∑ m ∈ Finset.range (n + 1), x ^ m * y ^ (n - m) * ↑(n.choose m)
Sources
Mathlibadd_pow
Uses 2 · Used by 9
Statement usesFinite set · Natural number
Used bySum of kth powers · Stirling’s Formula · Riemann-Lebesgue lemma (Analysis) · Behrend's construction · Frobenius morphism · Fernique's theorem · Fourier theorem · Poisson limit theorem · Cauchy formulas

TheoremThe Partition Theorem#

Mathlib states this as Nat.Partition.card_odds_eq_card_distincts.

Nat.Partition.card_odds_eq_card_distincts (n : ℕ) :
  (Nat.Partition.odds n).card = (Nat.Partition.distincts n).card
Sources
MathlibNat.Partition.card_odds_eq_card_distincts
Uses 3
Statement usesFinite set · Natural number
Proof usesGlaisher's theorem

TheoremThe Solution of the General Quartic Equation#

The Solution of Quartic. The roots of a quartic polynomial when q is nonzero. See Zwillinger. Here, u needs to satisfy the cubic resolvent. An explicit expression of u is possible using the cubic formula, but would be too long.

Theorems100.quartic_eq_zero_iff.{u_1} {K : Type u_1} [Field K] (a b c d e : K) {p q r s u v w : K}
  [Invertible 2] (ha : a ≠ 0) (hp : p = (8 * a * c - 3 * b ^ 2) / (8 * a ^ 2))
  (hq : q = (b ^ 3 - 4 * a * b * c + 8 * a ^ 2 * d) / (8 * a ^ 3)) (hq_nonzero : q ≠ 0)
  (hr : r = (16 * a * b ^ 2 * c + 256 * a ^ 3 * e - 3 * b ^ 4 - 64 * a ^ 2 * b * d) / (256 * a ^ 4))
  (hu : u ^ 3 - p * u ^ 2 - 4 * r * u + 4 * p * r - q ^ 2 = 0) (hs : s ^ 2 = u - p)
  (hv : v ^ 2 = 4 * s ^ 2 - 8 * (u - q / s)) (hw : w ^ 2 = 4 * s ^ 2 - 8 * (u + q / s)) (x : K) :
  a * x ^ 4 + b * x ^ 3 + c * x ^ 2 + d * x + e = 0 ↔
    x = (-2 * s - v) / 4 - b / (4 * a) ∨
      x = (-2 * s + v) / 4 - b / (4 * a) ∨
        x = (2 * s - w) / 4 - b / (4 * a) ∨ x = (2 * s + w) / 4 - b / (4 * a)
Sources
MathlibTheorems100.quartic_eq_zero_iff
Uses 6
Statement usesField · Invertible elements · Rational number
Proof usesCharacteristic zero · List · Local ring

TheoremDirichlet’s Theorem#

Dirichlet's Theorem on primes in arithmetic progression: if q is a positive integer and a : ZMod q is a unit, then there are infinitely many prime numbers p such that (p : ZMod q) = a.

Nat.infinite_setOfPred_prime_and_eq_mod {q : ℕ} [NeZero q] {a : ZMod q} (ha : IsUnit a) :
  {p | Nat.Prime p ∧ ↑p = a}.Infinite
Sources
MathlibNat.infinite_setOfPred_prime_and_eq_mod
Uses 13
Statement usesInteger · Irreducible element
Proof usesAbsolutely convergent series in Banach spaces · Arithmetic functions · Bezout’s Theorem · Characteristic p · Cyclic group · Divergence of the Prime Reciprocal Series · Euler's totient function (\(\varphi\)) · Extended real number · Fundamental theorem of algebra · Invertible elements · Separable polynomial

TheoremWilson’s Lemma#

Wilson's Lemma: the product of 1, ..., p-1 is -1 modulo p.

ZMod.wilsons_lemma (p : ℕ) [Fact (Nat.Prime p)] : ↑(p - 1).factorial = -1
Sources
MathlibZMod.wilsons_lemma
Uses 5 · Used by 1
Statement usesField · Irreducible element · Rational number
Proof usesFinite set · Group morphism
Used bySum of two squares

TheoremThe Number of Subsets of a Set#

Number of Subsets of a Set

Finset.card_powerset.{u_1} {α : Type u_1} (s : Finset α) : s.powerset.card = 2 ^ s.card
Sources
MathlibFinset.card_powerset
Uses 2 · Used by 2
Statement usesFinite set · Natural number
Used byDivergence of the Prime Reciprocal Series · Kleitman's theorem

TheoremKönigsberg Bridges Problem#

The Königsberg graph is not Eulerian.

Konigsberg.not_isEulerian {u v : Konigsberg.Verts} (p : Konigsberg.graph.Walk u v)
  (h : p.IsEulerian) : False
Sources
MathlibKonigsberg.not_isEulerian
Uses 5
Statement usesList · Natural number · Simple graph
Proof usesCharacteristic zero · Finite set

TheoremProduct of Segments of Chords#

Intersecting Chords Theorem.

EuclideanGeometry.mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_pi.{u_1, u_2} {V : Type u_1}
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] {P : Type u_2} [MetricSpace P]
  [NormedAddTorsor V P] {a b c d p : P} (h : EuclideanGeometry.Cospherical {a, b, c, d})
  (hapb : EuclideanGeometry.angle a p b = Real.pi)
  (hcpd : EuclideanGeometry.angle c p d = Real.pi) : dist a p * dist b p = dist c p * dist d p
Sources
MathlibEuclideanGeometry.mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_pi
Uses 7 · Used by 1
Statement usesAngle · Euclidean affine space
Proof usesAffine function · Affine span · Characteristic zero · Invertible elements · Ordered ring
Used byPtolemy’s Theorem

TheoremHeron’s Formula#

Heron's formula: The area of a triangle with side lengths a, b, and c is √(s * (s - a) * (s - b) * (s - c)) where s = (a + b + c) / 2 is the semiperimeter. We show this by equating this formula to a * b * sin γ, where γ is the angle opposite the side c.

Theorems100.heron.{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} (h1 : p₁ ≠ p₂)
  (h2 : p₃ ≠ p₂) :
  have a := dist p₁ p₂;
  have b := dist p₃ p₂;
  have c := dist p₁ p₃;
  have s := (a + b + c) / 2;
  1 / 2 * a * b * Real.sin (EuclideanGeometry.angle p₁ p₂ p₃) = √(s * (s - a) * (s - b) * (s - c))
Sources
MathlibTheorems100.heron
Uses 6
Statement usesAngle · Euclidean affine space
Proof usesCharacteristic zero · Euclidean domain · Ordered ring · The Law of Cosines

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.