nonuniformWitnesses_spec — Mathlib

English

If not ε-uniform, then the density gap |ρ(W1) − ρ(W2)| is bounded below by ε with a witness pair (W1,W2).

Русский

Если не существует ε-однородности, то разница плотностей между свидетелями W1 и W2 имеет нижнюю границу ε.

LaTeX

$$ε ≤ | G.edgeDensity (G.nonuniformWitnesses ε s t).fst (G.nonuniformWitnesses ε s t).snd − G.edgeDensity s t |$$

Lean4

theorem nonuniformWitnesses_spec (h : ¬G.IsUniform ε s t) :
    ε ≤ |G.edgeDensity (G.nonuniformWitnesses ε s t).1 (G.nonuniformWitnesses ε s t).2 - G.edgeDensity s t| :=
  by
  rw [nonuniformWitnesses, dif_pos h]
  exact (not_isUniform_iff.1 h).choose_spec.2.choose_spec.2.2.2

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