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

• 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 ADE_inequality.A' (q r : ℕ+) :

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

Equations
• = {1, q, r}
def ADE_inequality.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$.

Equations
def ADE_inequality.D' (r : ℕ+) :

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
• = {2, 2, r}
def ADE_inequality.E' (r : ℕ+) :

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
• = {2, 3, r}

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}) :
theorem ADE_inequality.admissible_of_one_lt_sum_inv_aux {pqr : list ℕ+} (hs : pqr) (hl : pqr.length = 3) (H : 1 < ) :

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}