theorem
ContagiousStructure.contagious_structure_mul
{Z : Type u_1}
[CommRing Z]
[IsDomain Z]
[DecidableEq Z]
(A : Finset Z)
(t₁ t₂ : Z)
(K : ℝ)
(hK : 0 ≤ K)
(ht₁ : t₁ ≠ 0)
(h₁ : ↑(A - t₁ • A).card ≤ K * ↑A.card)
(h₂ : ↑(A - t₂ • A).card ≤ K * ↑A.card)
:
Contagious structure lemma (multiplicative form). For a commutative domain Z,
a finite set A ⊆ Z, and nonzero scalars t₁, t₂, if |A − t₁·A| ≤ K|A| and
|A − t₂·A| ≤ K|A|, then |A − (t₁ · t₂)·A| ≤ K² |A|. This says that having
small dilated difference sets is "contagious" under products of the dilation
parameter.