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.

Equations

• ADEInequality.A' q r = {1, q, r}

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

Equations

• ADEInequality.A r = ADEInequality.A' 1 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}$.

Equations

• ADEInequality.D' r = {2, 2, r}

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

Equations

• ADEInequality.E' r = {2, 3, r}

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

Equations

• ADEInequality.E6 = ADEInequality.E' 3

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

Equations

• ADEInequality.E7 = ADEInequality.E' 4

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

Equations

• ADEInequality.E8 = ADEInequality.E' 5

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.

Equations

• ADEInequality.sumInv pqr = (Multiset.map (fun (x : ℕ+) => (↑↑x)⁻¹) pqr).sum

theorem ADEInequality.sumInv_pqr (p : ℕ+) (q : ℕ+) (r : ℕ+) : ADEInequality.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.

Equations

• One or more equations did not get rendered due to their size.

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

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

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

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

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

theorem ADEInequality.admissible_E6 : ADEInequality.Admissible ADEInequality.E6

theorem ADEInequality.admissible_E7 : ADEInequality.Admissible ADEInequality.E7

theorem ADEInequality.admissible_E8 : ADEInequality.Admissible ADEInequality.E8

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

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}) : ADEInequality.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 < ADEInequality.sumInv ↑pqr → ADEInequality.Admissible ↑pqr

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

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