English
For finite A,B,C in a group G, the divisional Plünnecke inequality yields
Русский
Для конечных A,B,C в группе G выполняется неравенство, связывающее деления и произведения.
LaTeX
$$$\#(A / C) \cdot \#B \le \#(A / B) \cdot \#(B \cdot C)$$$
Lean4
/-- The **Plünnecke-Ruzsa inequality**. Multiplication version. Note that this is genuinely harder
than the division version because we cannot use a double counting argument. -/
@[to_additive /-- The **Plünnecke-Ruzsa inequality**. Addition version. Note that this is genuinely
harder than the subtraction version because we cannot use a double counting argument. -/
]
theorem pluennecke_ruzsa_inequality_pow_div_pow_mul (hA : A.Nonempty) (B : Finset G) (m n : ℕ) :
#(B ^ m / B ^ n) ≤ (#(A * B) / #A : ℚ≥0) ^ (m + n) * #A :=
by
have hA' : A ∈ A.powerset.erase ∅ := mem_erase_of_ne_of_mem hA.ne_empty (mem_powerset_self _)
obtain ⟨C, hC, hCmin⟩ := exists_min_image (A.powerset.erase ∅) (fun C ↦ #(C * B) / #C : _ → ℚ≥0) ⟨A, hA'⟩
rw [mem_erase, mem_powerset, ← nonempty_iff_ne_empty] at hC
obtain ⟨hC, hCA⟩ := hC
refine le_of_mul_le_mul_right ?_ (by positivity : (0 : ℚ≥0) < #C)
calc
(#(B ^ m / B ^ n) * #C : ℚ≥0) ≤ #(B ^ m * C) * #(B ^ n * C) := mod_cast ruzsa_triangle_inequality_div_mul_mul ..
_ = #(C * B ^ m) * #(C * B ^ n) := by simp_rw [mul_comm]
_ ≤ ((#(C * B) / #C) ^ m * #C) * ((#(C * B) / #C : ℚ≥0) ^ n * #C) := by
gcongr <;> exact card_mul_pow_le (mul_aux hC hCA hCmin) _
_ = (#(C * B) / #C) ^ (m + n) * #C * #C := by ring
_ ≤ (#(A * B) / #A) ^ (m + n) * #A * #C := by gcongr (?_ ^ _) * #?_ * _; exact hCmin _ hA'
