English
Ruzsa's triangle inequality in division form: for finite A,B,C in a group, |A/C| |B| ≤ |A/B| |C/B|.
Русский
Неравенство треугольника Рузы в форме деления: для конечных A,B,C в группе: |A/C|·|B| ≤ |A/B|·|C/B|.
LaTeX
$$$\\#(A/C) \\cdot \\#B \\leq \\#(A/B) \\cdot \\#(C/B)$$$
Lean4
/-- **Ruzsa's triangle inequality**. Division version. -/
@[to_additive /-- **Ruzsa's triangle inequality**. Subtraction version. -/
]
theorem ruzsa_triangle_inequality_div_div_div (A B C : Finset G) : #(A / C) * #B ≤ #(A / B) * #(C / B) :=
by
rw [← card_product (A / B), ← mul_one #((A / B) ×ˢ (C / B))]
refine
card_mul_le_card_mul (fun b (a, c) ↦ a / c = b) (fun x hx ↦ ?_) fun x _ ↦
card_le_one_iff.2 fun hu hv ↦ ((mem_bipartiteBelow _).1 hu).2.symm.trans ?_
· obtain ⟨a, ha, c, hc, rfl⟩ := mem_div.1 hx
refine card_le_card_of_injOn (fun b ↦ (a / b, c / b)) (fun b hb ↦ ?_) fun b₁ _ b₂ _ h ↦ ?_
· rw [mem_coe, mem_bipartiteAbove]
exact ⟨mk_mem_product (div_mem_div ha hb) (div_mem_div hc hb), div_div_div_cancel_right ..⟩
· exact div_right_injective (Prod.ext_iff.1 h).1
· exact ((mem_bipartiteBelow _).1 hv).2
