English
Let A, B, C be finite subsets of a group G. Then |A C| · |B| ≤ |A B| · |B C|.
Русский
Пусть A, B, C — конечные подмножества группы G. Тогда |A C| · |B| ≤ |A B| · |B C|.
LaTeX
$$$|A C|\,|B| \le |A B|\,|B C|$$$
Lean4
/-- **Ruzsa's triangle inequality**. Multiplication version. -/
@[to_additive /-- **Ruzsa's triangle inequality**. Addition version. -/
]
theorem ruzsa_triangle_inequality_mul_mul_mul (A B C : Finset G) : #(A * C) * #B ≤ #(A * B) * #(B * C) :=
by
obtain rfl | hB := B.eq_empty_or_nonempty
· simp
have hB' : B ∈ B.powerset.erase ∅ := mem_erase_of_ne_of_mem hB.ne_empty (mem_powerset_self _)
obtain ⟨U, hU, hUA⟩ := exists_min_image (B.powerset.erase ∅) (fun U ↦ #(U * A) / #U : _ → ℚ≥0) ⟨B, hB'⟩
rw [mem_erase, mem_powerset, ← nonempty_iff_ne_empty] at hU
refine cast_le.1 (?_ : (_ : ℚ≥0) ≤ _)
push_cast
rw [← le_div_iff₀ (cast_pos.2 hB.card_pos), mul_div_right_comm, mul_comm _ B]
refine (Nat.cast_le.2 <| card_le_card_mul_left hU.1).trans ?_
refine
le_trans ?_
(mul_le_mul (hUA _ hB') (cast_le.2 <| card_le_card <| mul_subset_mul_right hU.2) (zero_le _) (zero_le _))
rw [← mul_div_right_comm, ← mul_assoc, le_div_iff₀ (cast_pos.2 hU.1.card_pos), mul_comm _ C, ← mul_assoc,
mul_comm _ C]
exact mod_cast pluennecke_petridis_inequality_mul C (mul_aux hU.1 hU.2 hUA)
