mulDysonETransform — Mathlib

English

Another formulation of the δ ≤ σ^2 bound under different normalizations; δ_m[A] ≤ σ_m[A]^2.

Русский

Другая формулировка неравенства δ ≤ σ^2 в другой нормализации; δ_m[A] ≤ σ_m[A]^2.

LaTeX

$$\\delta_m[A] \\le \\sigma_m[A]^2$$

Lean4

/-- The **Dyson e-transform**. Turns `(s, t)` into `(s ∪ e • t, t ∩ e⁻¹ • s)`. This reduces the
product of the two sets. -/
@[to_additive (attr := simps) /-- The **Dyson e-transform**.
    Turns `(s, t)` into `(s ∪ e +ᵥ t, t ∩ -e +ᵥ s)`. This reduces the sum of the two sets. -/
    ]
def mulDysonETransform : Finset α × Finset α :=
  (x.1 ∪ e • x.2, x.2 ∩ e⁻¹ • x.1)

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