noncomputable def BSG.pathCount₃ {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (A : Finset α) (B : Finset β) (X : Finset (α × β)) (a : α) (b : β) : ℕ

pathCount₃ A B X a b is the number of length-3 paths a — b₁ — a₁ — b in the bipartite graph with edge set X ⊆ A × B.

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

pathCount₂ B X a₁ a₂ counts common neighbours in B of a₁ and a₂, i.e. the number of b ∈ B with (a₁, b), (a₂, b) ∈ X — equivalently $P_2(a_1, a_2)$.

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

The co-neighbours of b ∈ B inside A: elements a ∈ A with (a, b) ∈ X.

noncomputable def BSG.neighbors' {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (X : Finset (α × β)) (a : α) (B : Finset β) : Finset β

The neighbours of a ∈ A inside B: elements b ∈ B with (a, b) ∈ X.

theorem BSG.eps_bad_pairs_lemma {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (A : Finset α) (B : Finset β) (X : Finset (α × β)) (hX_sub : X ⊆ A ×ˢ B) (K : ℝ) (hK : K > 0) (hX : ↑X.card ≥ K⁻¹ * ↑A.card * ↑B.card) (ε : ℝ) (hε : ε > 0) : ∃ A' ⊆ A, ↑A'.card ≥ 1 / 4 * K⁻¹ * ↑A.card ∧ (∀ a ∈ A', ↑(neighbors' X a B).card ≥ 1 / 10 * K⁻¹ * ↑B.card) ∧ ∀ a ∈ A', ↑{a₂ ∈ A' | ↑(pathCount₂ B X a a₂) < ε * K⁻¹ ^ 2 * ↑B.card}.card ≤ 10 * ε * ↑A'.card

ε-bad pairs lemma (preparation for BSG). If X ⊆ A × B has density ≥ K⁻¹|A||B| and ε > 0, there is a refinement A' ⊆ A of size ≥ ¼ K⁻¹ |A| such that:

• every a ∈ A' has many neighbours in B (at least (1/10) K⁻¹ |B|), and
• for every a ∈ A', only ≤ 10 ε |A'| of the elements a₂ ∈ A' are ε-bad relative to a, i.e. share fewer than ε K⁻² |B| common neighbours with a.

theorem BSG.min_degree_of_dense_subset {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (A : Finset α) (B : Finset β) (X : Finset (α × β)) (_hX_sub : X ⊆ A ×ˢ B) (K : ℝ) (_hK : K ≥ 1) (_hX_dense : ↑X.card ≥ K⁻¹ * ↑A.card * ↑B.card) (ε : ℝ) (_hε : ε > 0) (A' : Finset α) (_hA'_sub : A' ⊆ A) (_hA'_card : ↑A'.card ≥ 1 / 4 * K⁻¹ * ↑A.card) (hA'_deg : ∀ a ∈ A', ↑(neighbors' X a B).card ≥ 1 / 10 * K⁻¹ * ↑B.card) (_hA'_bad : ∀ a ∈ A', ↑{a₂ ∈ A' | ↑(pathCount₂ B X a a₂) < ε * K⁻¹ ^ 2 * ↑B.card}.card ≤ 10 * ε * ↑A'.card) (a : α) : a ∈ A' → ↑(neighbors' X a B).card ≥ 1 / 10 * K⁻¹ * ↑B.card

Trivial repackaging: the minimum-degree property guaranteed by eps_bad_pairs_lemma on A' is preserved (used as a clean hypothesis-passing wrapper).

theorem BSG.exists_zpow_neg_le (K : ℝ) (hK : K > 1) (r : ℝ) (hr : r > 0) : ∃ (c : ℕ), K ^ (-↑c) ≤ r

For any K > 1 and r > 0, some negative integer power K^(-c) is ≤ r. Used to absorb the constants in the BSG key lemma into the exponent -c.

theorem BSG.pathCount₃_ge_of_many_good {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (A : Finset α) (B : Finset β) (X : Finset (α × β)) (a : α) (b : β) (S : Finset α) (t : ℕ) (hS_sub_A : S ⊆ A) (hS_conn_b : ∀ a₁ ∈ S, (a₁, b) ∈ X) (hS_paths : ∀ a₁ ∈ S, pathCount₂ B X a a₁ ≥ t) : pathCount₃ A B X a b ≥ S.card * t

Lower bound on pathCount₃. If S ⊆ A consists of vertices a₁ each connected to b and each sharing at least t common neighbours with a in B, then the number of length-3 paths from a to b is at least |S| · t.

theorem BSG.pathCount₃_of_complete {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (A : Finset α) (B : Finset β) (a : α) (b : β) (ha : a ∈ A) (hb : b ∈ B) : pathCount₃ A B (A ×ˢ B) a b = B.card * A.card

For the complete bipartite graph X = A × B, the number of length-3 paths between any a ∈ A and b ∈ B is exactly |B| · |A|.

theorem BSG.density_bound_of_good_sets {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (A : Finset α) (B : Finset β) (X : Finset (α × β)) (hX_sub : X ⊆ A ×ˢ B) (K : ℝ) (hK_gt : K > 1) (A' : Finset α) (hA'_sub : A' ⊆ A) (hA'_card : ↑A'.card ≥ 1 / 4 * K⁻¹ * ↑A.card) (hA'_deg : ∀ a ∈ A', ↑(neighbors' X a B).card ≥ 1 / 10 * K⁻¹ * ↑B.card) (ε : ℝ) (hε_pos : ε > 0) (hε_def : ε = 10⁻¹ ^ 6 * K⁻¹ ^ 2) (B' : Finset β) (hB'_def : B' = {b ∈ B | ↑(coNeighbors X b A').card > 20 * ε * ↑A'.card}) : ↑{p ∈ X | p.1 ∈ A' ∧ p.2 ∈ B'}.card ≥ 1 / 80 * K⁻¹ ^ 2 * ↑A.card * ↑B.card

Density bound for (A', B') after BSG refinement. Restricting X to pairs in A' × B', with B' being the set of b ∈ B having many A'-co-neighbours, retains a positive fraction of the original density: $|X \cap (A' \times B')| \ge \tfrac{1}{80} K^{-2} |A| |B|$.

theorem BSG.path_count_bound_of_good_sets {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (A : Finset α) (B : Finset β) (X : Finset (α × β)) (hX_sub : X ⊆ A ×ˢ B) (K : ℝ) (hK_gt : K > 1) (A' : Finset α) (hA'_sub : A' ⊆ A) (hA'_card : ↑A'.card ≥ 1 / 4 * K⁻¹ * ↑A.card) (ε : ℝ) (hε_pos : ε > 0) (hA'_bad : ∀ a ∈ A', ↑{a₂ ∈ A' | ↑(pathCount₂ B X a a₂) < ε * K⁻¹ ^ 2 * ↑B.card}.card ≤ 10 * ε * ↑A'.card) (B' : Finset β) (hB'_def : B' = {b ∈ B | ↑(coNeighbors X b A').card > 20 * ε * ↑A'.card}) (a : α) (ha : a ∈ A') (b : β) (hb : b ∈ B') : ↑(pathCount₃ A B X a b) ≥ 10 / 4 * ε ^ 2 * K⁻¹ ^ 2 * (1 / 4) * K⁻¹ * ↑A.card * ↑B.card

Path-count bound for (A', B') after BSG refinement. For every a ∈ A' and b ∈ B', the number of length-3 paths from a to b is large: $\operatorname{pathCount}_3(A, B, X, a, b) \ge \tfrac{10}{16} \varepsilon^2 K^{-3} |A| |B|$.

theorem BSG.key_lemma_bsg {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (A : Finset α) (B : Finset β) (X : Finset (α × β)) (hX_sub : X ⊆ A ×ˢ B) (K : ℝ) (hK : K ≥ 1) (hX_dense : ↑X.card ≥ K⁻¹ * ↑A.card * ↑B.card) : ∃ (c : ℕ) (A' : Finset α) (B' : Finset β), A' ⊆ A ∧ B' ⊆ B ∧ ↑{p ∈ X | p.1 ∈ A' ∧ p.2 ∈ B'}.card ≥ K ^ (-↑c) * ↑A.card * ↑B.card ∧ ∀ a ∈ A', ∀ b ∈ B', ↑(pathCount₃ A B X a b) ≥ K ^ (-↑c) * ↑A.card * ↑B.card

Lemma (Key Lemma) for Balog–Szemerédi–Gowers. If X ⊆ A × B has density |X| ≥ K⁻¹ |A| |B|, then there exist refinements A' ⊆ A, B' ⊆ B and an exponent c ∈ ℕ such that the restriction of X to A' × B' still has density ≥ K^{-c} |A||B| and every pair (a, b) ∈ A' × B' is joined by at least K^{-c} |A||B| length-3 paths in the bipartite graph defined by X.