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

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.

• 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}

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

## Main declarations #

• pqr.A' q r, the multiset {1,q,r}
• pqr.D' r, the multiset {2,2,r}
• pqr.E6, the multiset {2,3,3}
• pqr.E7, the multiset {2,3,4}
• pqr.E8, the multiset {2,3,5}
• pqr.classification, the classification of solutions to p⁻¹ + q⁻¹ + r⁻¹ > 1
def ADEInequality.A' (q : ℕ+) (r : ℕ+) :

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

Instances For
def ADEInequality.A (r : ℕ+) :

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$.

Instances For

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}$.

Instances For

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}$.

Instances For

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$.

Instances For

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$.

Instances For

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$.

Instances For

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.

Instances For
theorem ADEInequality.sumInv_pqr (p : ℕ+) (q : ℕ+) (r : ℕ+) :
ADEInequality.sumInv {p, q, r} = (p)⁻¹ + (q)⁻¹ + (r)⁻¹

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.

Instances For
theorem ADEInequality.lt_three {p : ℕ+} {q : ℕ+} {r : ℕ+} (hpq : p q) (hqr : q r) (H : 1 < ADEInequality.sumInv {p, q, r}) :
p < 3
theorem ADEInequality.lt_four {q : ℕ+} {r : ℕ+} (hqr : q r) (H : 1 < ADEInequality.sumInv {2, q, r}) :
q < 4
theorem ADEInequality.lt_six {r : ℕ+} (H : 1 < ADEInequality.sumInv {2, 3, r}) :
r < 6
theorem ADEInequality.admissible_of_one_lt_sumInv_aux' {p : ℕ+} {q : ℕ+} {r : ℕ+} (hpq : p q) (hqr : q r) (H : 1 < ADEInequality.sumInv {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}