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

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

## Main declarations #

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.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 x x_1 => x ≤ x_1) pqr →
List.length pqr = 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: