AdditiveEnergy
The number of quadruples with .
mathlib4
Finset.addEnergyAdditiveEnergy(A, B), the pairs of pairs with equal sums.AdditiveEnergy(A).Typed signatures
| Type | Package | Applies |
|---|---|---|
(collection, collection?) -> integer | combinatorics | always |
Details
- Defined in Epsil as , where is the number of pairs with : two pairs with the same sum are one quadruple, so tallying the sums is enough and the quadruples are never tested.
- The members are the distinct members of the collection, as in mathlib's
Finset: a list's repeats are ignored, and a Set reads like a list. - Members must be exact rationals. A float, a symbol or an infinite collection leaves the call unevaluated, since a sum of floats would be tallied by rounding.
- At most , since a sum has at most that many representations, and a subgroup reaches . A Sidon set has the least for its size, ; large energy is what marks a set as additively structured.
- , and an arithmetic progression, translated or dilated, has the same energy.
- Symmetric in its two arguments, and unchanged by translating either set.
- Not a Wolfram, SymPy or Sage head. MultiplicativeEnergy is the same count for products.
Examples
1 more kept as data, checked against the oraclesScope #
Properties #
About
| Examples | 13 |
|---|---|
| Checked against | mathlib4 13 agree |
| Crosswalk | mathlib4 |
Implementation
mapped
mathlib4packages/oracle/src/mappings.tsmathlib's energy is over Finsets, so each list is read as a Finset of rationals (duplicates collapse, as ours do)
mapped
mathlib4packages/oracle/src/mappings.tsmathlib's energy is over Finsets, so each list is read as a Finset of rationals (duplicates collapse, as ours do)
See also: MultiplicativeEnergy, Tally, Unique