ADEInequality.classification
theorem ADEInequality.classification :
∀ (p q r : ℕ+), 1 < ADEInequality.sumInv {p, q, r} ↔ ADEInequality.Admissible {p, q, r}
The ADE inequality theorem states that for any three positive natural numbers p, q, and r, the sum of their inverse values is greater than 1 if and only if the multiset {p, q, r} is admissible. Here, a multiset is considered admissible if it is of the form {1, q, r}, or {2, 2, r}, or one of the sets {2, 3, 3}, {2, 3, 4}, or {2, 3, 5}.
More concisely: The ADE inequality holds if and only if the multiset {p, q, r} of positive natural numbers satisfies 1/p + 1/q + 1/r > 1 if and only if it is admissible, i.e., {1, q, r} or {2, 2, r} or one of {2, 3, 3}, {2, 3, 4}, or {2, 3, 5}.
|
ADEInequality.sumInv_pqr
theorem ADEInequality.sumInv_pqr : ∀ (p q r : ℕ+), ADEInequality.sumInv {p, q, r} = (↑↑p)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ := by
sorry
The theorem `ADEInequality.sumInv_pqr` states that for any three positive natural numbers `p`, `q`, and `r`, the function `ADEInequality.sumInv` applied to the multiset `{p, q, r}` is equal to the sum of the inverses of `p`, `q`, and `r`, each treated as a rational number. This means that the function `sumInv` effectively computes the sum of the inverses of the elements in the multiset.
More concisely: For any multiset {p, q, r} of positive natural numbers, ADEInequality.sumInv({p, q, r}) = p^(-1) + q^(-1) + r^(-1).
|