English
If G is not ε-uniform on s,t, then there exist witnesses s'⊆s and t'⊆t with size-bounds and a lower bound on the density difference |ρ(s',t') − ρ(s,t)| relative to ε.
Русский
Если граф G не ε-однороден по отношению к s,t, существует пара подмножеств s'⊆s и t'⊆t, удовлетворяющих ограничениям по размерам и дающих нижнюю оценку по модулю разности плотностей.
LaTeX
$$$\neg G.IsUniform \varepsilon s t \iff \exists s' \subseteq s, \exists t' \subseteq t, \ #s \cdot \varepsilon \le |s'|,\ #t \cdot \varepsilon \le |t'|,\ \varepsilon \le \big| G.edgeDensity s' t' - G.edgeDensity s t \big|$$$
Lean4
theorem not_isUniform_iff :
¬G.IsUniform ε s t ↔
∃ s', s' ⊆ s ∧ ∃ t', t' ⊆ t ∧ #s * ε ≤ #s' ∧ #t * ε ≤ #t' ∧ ε ≤ |G.edgeDensity s' t' - G.edgeDensity s t| :=
by
unfold IsUniform
simp only [not_forall, not_lt, exists_prop, Rat.cast_abs, Rat.cast_sub]
