def BSG.neighborhood {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (X : Finset (α × β)) (b : β) : Finset α

The neighborhood N(b) = {a ∈ α : (a, b) ∈ X} of an element b ∈ β in a bipartite relation X ⊆ α × β.

def BSG.codegree {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (X : Finset (α × β)) (a₁ a₂ : α) : ℕ

The codegree P₂(a₁, a₂) := #{b ∈ β : (a₁, b) ∈ X ∧ (a₂, b) ∈ X} — the number of common neighbors of a₁ and a₂ in the bipartite relation X.

def BSG.IsEpsilonBad {α : Type u_1} {β : Type u_2} [Fintype β] [DecidableEq α] [DecidableEq β] (X : Finset (α × β)) (K ε : ℝ) (a₁ a₂ : α) : Prop

Definition (ε-bad pair). A pair (a₁, a₂) is ε-bad (relative to K) if P₂(a₁, a₂) < ε · K⁻² · |β|, i.e. the codegree is unusually small compared with the typical scale K⁻² |β|.

@[implicit_reducible]

noncomputable instance BSG.instDecidableIsEpsilonBad {α : Type u_1} {β : Type u_2} [Fintype β] [DecidableEq α] [DecidableEq β] (X : Finset (α × β)) (K ε : ℝ) (a₁ a₂ : α) : Decidable (IsEpsilonBad X K ε a₁ a₂)

Decidability of the ε-bad predicate (used to define the badness counting function below).

noncomputable def BSG.badPairsCount {α : Type u_1} {β : Type u_2} [Fintype β] [DecidableEq α] [DecidableEq β] (X : Finset (α × β)) (K ε : ℝ) (b : β) : ℕ

The bad-pairs counting function BP_ε(b) = #{(a₁, a₂) ∈ N(b)² : (a₁, a₂) is ε-bad} from the BSG analysis.