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.

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

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

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

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

                  Equations
                  • One or more equations did not get rendered due to their size.
                  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}) :
                    theorem ADEInequality.admissible_of_one_lt_sumInv_aux {pqr : List ℕ+} :
                    List.Sorted (fun (x1 x2 : ℕ+) => x1 x2) pqrpqr.length = 31 < ADEInequality.sumInv pqrADEInequality.Admissible pqr

                    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}