theorem IsApproximateSubgroup.pi {ι : Type u_2} {G : ι → Type u_3} [Fintype ι] [(i : ι) → Group (G i)] {A : (i : ι) → Set (G i)} {K : ι → ℝ} (hA : ∀ (i : ι), IsApproximateSubgroup (K i) (A i)) : IsApproximateSubgroup (∏ i : ι, K i) (Set.univ.pi A)

theorem IsApproximateAddSubgroup.pi {ι : Type u_2} {G : ι → Type u_3} [Fintype ι] [(i : ι) → AddGroup (G i)] {A : (i : ι) → Set (G i)} {K : ι → ℝ} (hA : ∀ (i : ι), IsApproximateAddSubgroup (K i) (A i)) : IsApproximateAddSubgroup (∏ i : ι, K i) (Set.univ.pi A)

theorem exists_isApproximateSubgroup_of_small_doubling {G : Type u_1} [Group G] {K : ℝ} [DecidableEq G] {A : Finset G} (hA₀ : A.Nonempty) (hA : ↑(A ^ 2).card ≤ K * ↑A.card) : ∃ S ⊆ (A⁻¹ * A) ^ 2, IsApproximateSubgroup (2 ^ 12 * K ^ 36) ↑S ∧ ↑S.card ≤ 16 * K ^ 12 * ↑A.card ∧ ∃ a ∈ A, ↑A.card / (2 * K) ≤ ↑(A ∩ MulOpposite.op a • S).card

theorem exists_isApproximateAddSubgroup_of_small_doubling {G : Type u_1} [AddGroup G] {K : ℝ} [DecidableEq G] {A : Finset G} (hA₀ : A.Nonempty) (hA : ↑(2 • A).card ≤ K * ↑A.card) : ∃ S ⊆ 2 • (-A + A), IsApproximateAddSubgroup (2 ^ 12 * K ^ 36) ↑S ∧ ↑S.card ≤ 16 * K ^ 12 * ↑A.card ∧ ∃ a ∈ A, ↑A.card / (2 * K) ≤ ↑(A ∩ (AddOpposite.op a +ᵥ S)).card