AdmitsFractional — Mathlib

English

A cost function f admits a fractional operation ω if applying the fractional operation to any compatible input lowers or preserves the total cost.

Русский

Функция стоимости f допускает фракционную операцию ω, если применение ω не увеличивает совокупную стоимость.

LaTeX

$$$\\forall x:(Fin n \\to D), m \\cdot ((\\omega.tt x).map f).sum \\le |\\omega| \\cdot \\sum_{i \\in \\mathsf{univ}} f(x(i))$$$

Lean4

/-- Cost function admits given fractional operation, i.e., `ω` improves `f` in the `≤` sense. -/
def AdmitsFractional {n : ℕ} (f : (Fin n → D) → C) (ω : FractionalOperation D m) : Prop :=
  ∀ x : (Fin m → (Fin n → D)), m • ((ω.tt x).map f).sum ≤ ω.size • Finset.univ.sum (fun i => f (x i))

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