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

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

## Instances For

`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

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

## Equations

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

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

## Equations

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

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

.

## Equations

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

## Instances For

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: