mathlib3 documentation

number_theory.ADE_inequality

The inequality `p⁻¹ + q⁻¹ + r⁻¹ > 1` #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 ADE_inequality.A' (q r : ℕ+) :

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

Equations

ADE_inequality.A' q r = {1, q, r}

def ADE_inequality.A (r : ℕ+) :

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

ADE_inequality.A r = ADE_inequality.A' 1 r

def ADE_inequality.D' (r : ℕ+) :

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

ADE_inequality.D' r = {2, 2, r}

def ADE_inequality.E' (r : ℕ+) :

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

ADE_inequality.E' r = {2, 3, r}

def ADE_inequality.E6 :

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

ADE_inequality.E6 = ADE_inequality.E' 3

def ADE_inequality.E7 :

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

ADE_inequality.E7 = ADE_inequality.E' 4

def ADE_inequality.E8 :

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

ADE_inequality.E8 = ADE_inequality.E' 5

def ADE_inequality.sum_inv (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

ADE_inequality.sum_inv pqr = (multiset.map (λ (x : ℕ+), (↑x)⁻¹) pqr).sum

theorem ADE_inequality.sum_inv_pqr (p q r : ℕ+) :

ADE_inequality.sum_inv {p, q, r} = (↑p)⁻¹ + (↑q)⁻¹ + (↑r)⁻¹

def ADE_inequality.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

ADE_inequality.admissible pqr = ((∃ (q r : ℕ+), ADE_inequality.A' q r = pqr) ∨ (∃ (r : ℕ+), ADE_inequality.D' r = pqr) ∨ ADE_inequality.E' 3 = pqr ∨ ADE_inequality.E' 4 = pqr ∨ ADE_inequality.E' 5 = pqr)

theorem ADE_inequality.admissible_A' (q r : ℕ+) :

ADE_inequality.admissible (ADE_inequality.A' q r)

theorem ADE_inequality.admissible_D' (n : ℕ+) :

ADE_inequality.admissible (ADE_inequality.D' n)

theorem ADE_inequality.admissible_E'3 :

ADE_inequality.admissible (ADE_inequality.E' 3)

theorem ADE_inequality.admissible_E'4 :

ADE_inequality.admissible (ADE_inequality.E' 4)

theorem ADE_inequality.admissible_E'5 :

ADE_inequality.admissible (ADE_inequality.E' 5)

theorem ADE_inequality.admissible_E6 :

ADE_inequality.admissible ADE_inequality.E6

theorem ADE_inequality.admissible_E7 :

ADE_inequality.admissible ADE_inequality.E7

theorem ADE_inequality.admissible_E8 :

ADE_inequality.admissible ADE_inequality.E8

theorem ADE_inequality.admissible.one_lt_sum_inv {pqr : multiset ℕ+} :

ADE_inequality.admissible pqr → 1 < ADE_inequality.sum_inv pqr

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

p < 3

theorem ADE_inequality.lt_four {q r : ℕ+} (hqr : q ≤ r) (H : 1 < ADE_inequality.sum_inv {2, q, r}) :

q < 4

theorem ADE_inequality.lt_six {r : ℕ+} (H : 1 < ADE_inequality.sum_inv {2, 3, r}) :

r < 6

theorem ADE_inequality.admissible_of_one_lt_sum_inv_aux' {p q r : ℕ+} (hpq : p ≤ q) (hqr : q ≤ r) (H : 1 < ADE_inequality.sum_inv {p, q, r}) :

ADE_inequality.admissible {p, q, r}

theorem ADE_inequality.admissible_of_one_lt_sum_inv_aux {pqr : list ℕ+} (hs : list.sorted has_le.le pqr) (hl : pqr.length = 3) (H : 1 < ADE_inequality.sum_inv ↑pqr) :

ADE_inequality.admissible ↑pqr

theorem ADE_inequality.admissible_of_one_lt_sum_inv {p q r : ℕ+} (H : 1 < ADE_inequality.sum_inv {p, q, r}) :

ADE_inequality.admissible {p, q, r}

theorem ADE_inequality.classification (p q r : ℕ+) :

1 < ADE_inequality.sum_inv {p, q, r} ↔ ADE_inequality.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}