theorem BSG {G : Type u_1} [AddCommGroup G] [DecidableEq G] {A B : Finset G} [Finite G] {K : ℝ} (hK : 0 ≤ K) (hB : B.Nonempty) (hAB : K⁻¹ * (↑A.card ^ 2 * ↑B.card) ≤ ↑(A.addEnergy B)) : ∃ A' ⊆ A, (2 ^ 4)⁻¹ * K⁻¹ * ↑A.card ≤ ↑A'.card ∧ ↑(A' - A').card ≤ 2 ^ 10 * K ^ 5 * ↑B.card ^ 4 / ↑A.card ^ 3

theorem BSG₂ {G : Type u_1} [AddCommGroup G] [DecidableEq G] {A B : Finset G} [Finite G] {K : ℝ} (hK : 0 ≤ K) (hB : B.Nonempty) (hAB : K⁻¹ * (↑A.card ^ 2 * ↑B.card) ≤ ↑(A.addEnergy B)) : ∃ A' ⊆ A, ∃ B' ⊆ B, (2 ^ 4)⁻¹ * K⁻¹ * ↑A.card ≤ ↑A'.card ∧ (2 ^ 4)⁻¹ * K⁻¹ * ↑A.card ≤ ↑B'.card ∧ ↑(A' - B').card ≤ 2 ^ 10 * K ^ 5 * ↑B.card ^ 4 / ↑A.card ^ 3

theorem BSG_self {G : Type u_1} [AddCommGroup G] [DecidableEq G] {A : Finset G} [Finite G] {K : ℝ} (hK : 0 ≤ K) (hA : A.Nonempty) (hAK : K⁻¹ * ↑A.card ^ 3 ≤ ↑(A.addEnergy A)) : ∃ A' ⊆ A, (2 ^ 4)⁻¹ * K⁻¹ * ↑A.card ≤ ↑A'.card ∧ ↑(A' - A').card ≤ 2 ^ 10 * K ^ 5 * ↑A.card

theorem BSG_self' {G : Type u_1} [AddCommGroup G] [DecidableEq G] {A : Finset G} [Finite G] {K : ℝ} (hK : 0 ≤ K) (hA : A.Nonempty) (hAK : K⁻¹ * ↑A.card ^ 3 ≤ ↑(A.addEnergy A)) : ∃ A' ⊆ A, (2 ^ 4)⁻¹ * K⁻¹ * ↑A.card ≤ ↑A'.card ∧ ↑(A' - A').card ≤ 2 ^ 14 * K ^ 6 * ↑A'.card