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 : ℕ+) : Multiset ℕ+

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

def ADEInequality.A (r : ℕ+) : Multiset ℕ+

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

def ADEInequality.D' (r : ℕ+) : Multiset ℕ+

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

def ADEInequality.E' (r : ℕ+) : Multiset ℕ+

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

def ADEInequality.E6 : Multiset ℕ+

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

def ADEInequality.E7 : Multiset ℕ+

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

def ADEInequality.E8 : Multiset ℕ+

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

def ADEInequality.sumInv (pqr : Multiset ℕ+) : ℚ

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.

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

def ADEInequality.Admissible (pqr : Multiset ℕ+) : Prop

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.

theorem ADEInequality.admissible_A' (q r : ℕ+) : Admissible (A' q r)

theorem ADEInequality.admissible_D' (n : ℕ+) : Admissible (D' n)

theorem ADEInequality.admissible_E'3 : Admissible (E' 3)

theorem ADEInequality.admissible_E'4 : Admissible (E' 4)

theorem ADEInequality.admissible_E'5 : Admissible (E' 5)

theorem ADEInequality.admissible_E6 : Admissible E6

theorem ADEInequality.admissible_E7 : Admissible E7

theorem ADEInequality.admissible_E8 : Admissible E8

theorem ADEInequality.Admissible.one_lt_sumInv {pqr : Multiset ℕ+} : Admissible pqr → 1 < sumInv pqr

theorem ADEInequality.lt_three {p q r : ℕ+} (hpq : p ≤ q) (hqr : q ≤ r) (H : 1 < sumInv {p, q, r}) : p < 3

theorem ADEInequality.lt_four {q r : ℕ+} (hqr : q ≤ r) (H : 1 < sumInv {2, q, r}) : q < 4

theorem ADEInequality.lt_six {r : ℕ+} (H : 1 < 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 < sumInv {p, q, r}) : Admissible {p, q, r}

theorem ADEInequality.admissible_of_one_lt_sumInv_aux {pqr : List ℕ+} : List.Sorted (fun (x1 x2 : ℕ+) => x1 ≤ x2) pqr → pqr.length = 3 → 1 < sumInv ↑pqr → Admissible ↑pqr

theorem ADEInequality.admissible_of_one_lt_sumInv {p q r : ℕ+} (H : 1 < sumInv {p, q, r}) : Admissible {p, q, r}

theorem ADEInequality.classification (p q r : ℕ+) : 1 < sumInv {p, q, r} ↔ Admissible {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}