ruzsa_triangle_inequality_invMul_invMul_invMul

English

Ruzsa's triangle inequality with division and multiplication: #(A/C) · #B ≤ #(A·B) · #(C·B).

Русский

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

LaTeX

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

Lean4

/-- **Ruzsa's triangle inequality**. Invmul-invmul-invmul version. -/
@[to_additive /-- **Ruzsa's triangle inequality**. Negadd-negadd-negadd version. -/
    ]
theorem ruzsa_triangle_inequality_invMul_invMul_invMul (A B C : Finset G) : #B * #(A⁻¹ * C) ≤ #(B⁻¹ * A) * #(B⁻¹ * C) :=
  by
  simpa [mul_comm, div_eq_mul_inv, ← map_op_mul, ← map_op_inv] using
    ruzsa_triangle_inequality_div_div_div (G := Gᵐᵒᵖ) (C.map opEquiv.toEmbedding) (B.map opEquiv.toEmbedding)
      (A.map opEquiv.toEmbedding)

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