theorem BKTProof.card_sq_mul_card_sq_le_card_add_mul_addEnergy {α : Type u_1} [DecidableEq α] [Add α] (A B : Finset α) : A.card ^ 2 * B.card ^ 2 ≤ (A + B).card * A.addEnergy B

BKT additive energy proposition: for finite sets A, B in an additive group, |A|² · |B|² ≤ |A + B| · E(A, B), where E(A, B) denotes the additive energy of the pair. This is a thin wrapper around the corresponding Mathlib lemma.