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: