ruzsa_triangle_inequality_mul_div_mul

English

Ruzsa's triangle inequality in mul-div-mul form: #(B.card) · #(A·C) ≤ #(B·A) · #(B·C).

Русский

Неравенство Рузa в форме умножение-деление-умножение.

LaTeX

$$$ \\#B \\cdot \\#(A\\cdot C) \\leq \\#(B\\cdot A) \\cdot \\#(B\\cdot C)$$$

Lean4

/-- **Ruzsa's triangle inequality**. Mul-div-mul version. -/
@[to_additive /-- **Ruzsa's triangle inequality**. Add-sub-add version. -/
    ]
theorem ruzsa_triangle_inequality_mul_div_mul (A B C : Finset G) : #B * #(A * C) ≤ #(B / A) * #(B * C) := by
  simpa [div_eq_mul_inv] using ruzsa_triangle_inequality_invMul_mul_mul A⁻¹ B C

Похожие утверждения