Documentation

Mathlib.NumberTheory.ADEInequality

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.

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

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

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

        Instances For

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

          Instances For

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

            Instances For

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

              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.

                Instances For
                  theorem ADEInequality.sumInv_pqr (p : ℕ+) (q : ℕ+) (r : ℕ+) :
                  ADEInequality.sumInv {p, q, r} = (p)⁻¹ + (q)⁻¹ + (r)⁻¹

                  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.

                  Instances For
                    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}) :

                    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}