mathlib3 documentation

number_theory.ADE_inequality

The inequality p⁻¹ + q⁻¹ + r⁻¹ > 1 #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we classify solutions to the inequality (p⁻¹ + q⁻¹ + r⁻¹ : ℚ) > 1, for positive natural numbers p, q, and r.

The solutions are exactly of the form.

This inequality shows up in Lie theory, in the classification of Dynkin diagrams, root systems, and semisimple Lie algebras.

Main declarations #

A' q r := {1,q,r} is a multiset ℕ+ that is a solution to the inequality (p⁻¹ + q⁻¹ + r⁻¹ : ℚ) > 1.

Equations

A r := {1,1,r} is a multiset ℕ+ that is a solution to the inequality (p⁻¹ + q⁻¹ + r⁻¹ : ℚ) > 1.

These solutions are related to the Dynkin diagrams $A_r$.

Equations

D' r := {2,2,r} is a multiset ℕ+ that is a solution to the inequality (p⁻¹ + q⁻¹ + r⁻¹ : ℚ) > 1.

These solutions are related to the Dynkin diagrams $D_{r+2}$.

Equations

E' r := {2,3,r} is a multiset ℕ+. For r ∈ {3,4,5} is a solution to the inequality (p⁻¹ + q⁻¹ + r⁻¹ : ℚ) > 1.

These solutions are related to the Dynkin diagrams $E_{r+3}$.

Equations

E6 := {2,3,3} is a multiset ℕ+ that is a solution to the inequality (p⁻¹ + q⁻¹ + r⁻¹ : ℚ) > 1.

This solution is related to the Dynkin diagrams $E_6$.

Equations

E7 := {2,3,4} is a multiset ℕ+ that is a solution to the inequality (p⁻¹ + q⁻¹ + r⁻¹ : ℚ) > 1.

This solution is related to the Dynkin diagrams $E_7$.

Equations

E8 := {2,3,5} is a multiset ℕ+ that is a solution to the inequality (p⁻¹ + q⁻¹ + r⁻¹ : ℚ) > 1.

This solution is related to the Dynkin diagrams $E_8$.

Equations

sum_inv pqr for a pqr : multiset ℕ+ is the sum of the inverses of the elements of pqr, as rational number.

The intended argument is a multiset {p,q,r} of cardinality 3.

Equations

A multiset pqr of positive natural numbers is admissible if it is equal to A' q r, or D' r, or one of E6, E7, or E8.

Equations
theorem ADE_inequality.lt_three {p q r : ℕ+} (hpq : p q) (hqr : q r) (H : 1 < ADE_inequality.sum_inv {p, q, r}) :
p < 3
theorem ADE_inequality.lt_four {q r : ℕ+} (hqr : q r) (H : 1 < ADE_inequality.sum_inv {2, q, r}) :
q < 4
theorem ADE_inequality.lt_six {r : ℕ+} (H : 1 < ADE_inequality.sum_inv {2, 3, r}) :
r < 6
theorem ADE_inequality.admissible_of_one_lt_sum_inv_aux' {p q r : ℕ+} (hpq : p q) (hqr : q r) (H : 1 < ADE_inequality.sum_inv {p, q, r}) :

A multiset {p,q,r} of positive natural numbers is a solution to (p⁻¹ + q⁻¹ + r⁻¹ : ℚ) > 1 if and only if it is admissible which means it is one of:

  • A' q r := {1,q,r}
  • D' r := {2,2,r}
  • E6 := {2,3,3}, or E7 := {2,3,4}, or E8 := {2,3,5}