nonuniformWitness — Mathlib

English

The nonuniform witness pair (W1,W2) satisfies the density gap bound, aligning with the witness spec.

Русский

Пара свидетелей неоднородности (W1, W2) удовлетворяет границе разности плотностей, согласуясь со спецификацией свидетелей.

LaTeX

$$ε ≤ | G.edgeDensity (G.nonuniformWitness ε s t) (G.nonuniformWitness ε t s) − G.edgeDensity s t |$$

Lean4

/-- Arbitrary witness of non-uniformity. `G.nonuniformWitness ε s t` and
`G.nonuniformWitness ε t s` form a pair of subsets witnessing the non-uniformity of `(s, t)`. If
`(s, t)` is uniform, returns `s`. -/
noncomputable def nonuniformWitness (ε : 𝕜) (s t : Finset α) : Finset α :=
  if WellOrderingRel s t then (G.nonuniformWitnesses ε s t).1 else (G.nonuniformWitnesses ε t s).2

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