A tripartite Turán theorem

If three vertex sets A, B, C of a graph have pairwise edge densities α = d(A, B), β = d(B, C), γ = d(A, C) with αβ + γ > 1, βγ + α > 1 and γα + β > 1, the graph contains a triangle with one vertex in each set (Bondy–Shen–Thomassé–Thomassen, 2006); in particular this holds when all three densities exceed 1/φ, since (1/φ)² + 1/φ = 1, and 1/φ is optimal. The sets need not be disjoint. Following the paper, a minimal weighted counterexample is reduced, by a Pareto argument on the neighbourhoods, to parts with at most two strictly incomparable vertices; the remaining configurations are closed by explicit inequalities (the final matching case is closed directly by linear arithmetic here rather than as in the paper).

Main results

• TripartiteTuran.exists_triangle_of_mul_add: densities with alpha*beta + gamma > 1 (and cyclic) force a triangle
• TripartiteTuran.exists_triangle: all three densities above 1/phi force a triangle

References

• J. A. Bondy, J. Shen, S. Thomassé and C. Thomassen, Density conditions for triangles in multipartite graphs, Combinatorica 26 (2006), 121–131 (Theorem 3).

noncomputable def TripartiteTuran.nbw {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] (x : V) (Y : Finset V) (q : V → ℝ) : ℝ

Weight of the neighbourhood of x inside Y for the weight function q.

Equations

• TripartiteTuran.nbw G x Y q = ∑ y ∈ Y, if G.Adj x y then q y else 0

noncomputable def TripartiteTuran.dd {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] (X Y : Finset V) (p q : V → ℝ) : ℝ

Weighted edge density between X (weights p) and Y (weights q).

Equations

• TripartiteTuran.dd G X Y p q = ∑ x ∈ X, p x * TripartiteTuran.nbw G x Y q

def TripartiteTuran.Cyc (α β γ : ℝ) : Prop

A cyclic triple of densities.

Equations

• TripartiteTuran.Cyc α β γ = (1 < α * β + γ ∧ 1 < β * γ + α ∧ 1 < γ * α + β)

def TripartiteTuran.NoTri {V : Type u_1} (G : SimpleGraph V) (A B C : Finset V) : Prop

No triangle with one vertex in each of A, B, C.

Equations

• TripartiteTuran.NoTri G A B C = ∀ a ∈ A, ∀ b ∈ B, ∀ c ∈ C, ¬(G.Adj a b ∧ G.Adj b c ∧ G.Adj a c)

theorem TripartiteTuran.dd_comm {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] (X Y : Finset V) (p q : V → ℝ) : dd G X Y p q = dd G Y X q p

theorem TripartiteTuran.nbw_nonneg {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] (x : V) (Y : Finset V) (q : V → ℝ) (hq : ∀ y ∈ Y, 0 ≤ q y) : 0 ≤ nbw G x Y q

theorem TripartiteTuran.dd_nonneg {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] (X Y : Finset V) (p q : V → ℝ) (hp : ∀ x ∈ X, 0 ≤ p x) (hq : ∀ y ∈ Y, 0 ≤ q y) : 0 ≤ dd G X Y p q

theorem TripartiteTuran.Cyc.rot {α β γ : ℝ} (h : Cyc α β γ) : Cyc β γ α

theorem TripartiteTuran.Cyc.swap {α β γ : ℝ} (h : Cyc α β γ) : Cyc α γ β

theorem TripartiteTuran.Cyc.mono {α β γ α' γ' : ℝ} (h : Cyc α β γ) (hβ : 0 ≤ β) (h0α : 0 ≤ α) (h0γ : 0 ≤ γ) (hα : α ≤ α') (hγ : γ ≤ γ') : Cyc α' β γ'

theorem TripartiteTuran.exists_kernel (u v u' v' : ℝ) : ∃ (a : ℝ) (b : ℝ), (a ≠ 0 ∨ b ≠ 0) ∧ 0 ≤ a * u + b * v ∧ 0 ≤ a * u' + b * v'

Any real 2 × 2 matrix has a nonzero vector (a, b) with nonnegative image.

theorem TripartiteTuran.pareto3 {V : Type u_1} [DecidableEq V] (s : Finset V) (p f g : V → ℝ) (hp : ∀ i ∈ s, 0 ≤ p i) (hs : ∑ i ∈ s, p i = 1) (h3 : 3 ≤ s.card) : ∃ i ∈ s, ∃ (p' : V → ℝ), (∀ x ∈ s.erase i, 0 ≤ p' x) ∧ ∑ x ∈ s.erase i, p' x = 1 ∧ ∑ x ∈ s, p x * f x ≤ ∑ x ∈ s.erase i, p' x * f x ∧ ∑ x ∈ s, p x * g x ≤ ∑ x ∈ s.erase i, p' x * g x

theorem TripartiteTuran.dom_reduce {V : Type u_1} [DecidableEq V] (s : Finset V) (p f g : V → ℝ) (hp : ∀ i ∈ s, 0 ≤ p i) (hs : ∑ i ∈ s, p i = 1) (i j : V) (hi : i ∈ s) (hj : j ∈ s) (hij : i ≠ j) (h1 : p i * f i ≤ p i * f j) (h2 : p i * g i ≤ p i * g j) : ∃ (p' : V → ℝ), (∀ x ∈ s.erase i, 0 ≤ p' x) ∧ ∑ x ∈ s.erase i, p' x = 1 ∧ ∑ x ∈ s, p x * f x ≤ ∑ x ∈ s.erase i, p' x * f x ∧ ∑ x ∈ s, p x * g x ≤ ∑ x ∈ s.erase i, p' x * g x

theorem TripartiteTuran.reduce_sum {V : Type u_1} [DecidableEq V] (s : Finset V) (p f g : V → ℝ) (hp : ∀ i ∈ s, 0 ≤ p i) (hs : ∑ i ∈ s, p i = 1) (hred : 3 ≤ s.card ∨ ∃ i ∈ s, ∃ j ∈ s, i ≠ j ∧ p i * f i ≤ p i * f j ∧ p i * g i ≤ p i * g j) : ∃ i ∈ s, ∃ (p' : V → ℝ), (∀ x ∈ s.erase i, 0 ≤ p' x) ∧ ∑ x ∈ s.erase i, p' x = 1 ∧ ∑ x ∈ s, p x * f x ≤ ∑ x ∈ s.erase i, p' x * f x ∧ ∑ x ∈ s, p x * g x ≤ ∑ x ∈ s.erase i, p' x * g x

structure TripartiteTuran.Good {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] (A B C : Finset V) (p q r : V → ℝ) : Prop

A weighted tripartite configuration: triangle-free and cyclic.

• neA : A.Nonempty
• neB : B.Nonempty
• neC : C.Nonempty
• pA (a : V) : a ∈ A → 0 ≤ p a
• qB (b : V) : b ∈ B → 0 ≤ q b
• rC (c : V) : c ∈ C → 0 ≤ r c
• sA : ∑ a ∈ A, p a = 1
• sB : ∑ b ∈ B, q b = 1
• sC : ∑ c ∈ C, r c = 1
• nt : NoTri G A B C
• cyc : Cyc (dd G A B p q) (dd G B C q r) (dd G A C p r)

def TripartiteTuran.Red {V : Type u_1} {G : SimpleGraph V} [DecidableRel G.Adj] (s : Finset V) (p : V → ℝ) (Y : Finset V) (q : V → ℝ) (Z : Finset V) (r : V → ℝ) : Prop

The part s (weights p, other parts Y, Z) can be shrunk: it has ≥ 3 vertices, or some vertex i is dominated by another one j (weighted by p i).

Equations

• One or more equations did not get rendered due to their size.

theorem TripartiteTuran.Good.reduce {V : Type u_1} {G : SimpleGraph V} [DecidableRel G.Adj] [DecidableEq V] {A B C : Finset V} {p q r : V → ℝ} (h : Good G A B C p q r) (hr : Red A p B q C r) : ∃ (A' : Finset V) (p' : V → ℝ), A'.card < A.card ∧ Good G A' B C p' q r

theorem TripartiteTuran.Good.rot {V : Type u_1} {G : SimpleGraph V} [DecidableRel G.Adj] {A B C : Finset V} {p q r : V → ℝ} (h : Good G A B C p q r) : Good G B C A q r p

theorem TripartiteTuran.Good.swap {V : Type u_1} {G : SimpleGraph V} [DecidableRel G.Adj] {A B C : Finset V} {p q r : V → ℝ} (h : Good G A B C p q r) : Good G B A C q p r

theorem TripartiteTuran.nbw_le_sum {V : Type u_1} {G : SimpleGraph V} [DecidableRel G.Adj] (x : V) (Y : Finset V) (q : V → ℝ) (hq : ∀ y ∈ Y, 0 ≤ q y) : nbw G x Y q ≤ ∑ y ∈ Y, q y

theorem TripartiteTuran.nbw_add_le {V : Type u_1} {G : SimpleGraph V} [DecidableRel G.Adj] {a b : V} (hab : G.Adj a b) (C : Finset V) (r : V → ℝ) (hr : ∀ c ∈ C, 0 ≤ r c) (hnt : ∀ c ∈ C, ¬(G.Adj a b ∧ G.Adj b c ∧ G.Adj a c)) : nbw G a C r + nbw G b C r ≤ ∑ c ∈ C, r c

theorem TripartiteTuran.case2_alg (α β γ b a c : ℝ) (hb0 : 0 < b) (hb1 : b < 1) (ha0 : 0 ≤ a) (ha1 : a ≤ 1) (hc0 : 0 ≤ c) (hc1 : c ≤ 1) (hβ : β = b * c) (hα : α ≤ b * a + (1 - b)) (hγ : γ ≤ 1 - a * c) (h1 : 1 < α * β + γ) (h2 : 1 < β * γ + α) : False

Algebra of case 2 of BSTT: a vertex b₂ of B = {b₁, b₂} without neighbours in C.

theorem TripartiteTuran.Good.no_missing {V : Type u_1} {G : SimpleGraph V} [DecidableRel G.Adj] {A B C : Finset V} {p q r : V → ℝ} [DecidableEq V] (h : Good G A B C p q r) (b1 b2 : V) (hB : B = {b1, b2}) (hne : b1 ≠ b2) (hq1 : 0 < q b1) (hq2 : 0 < q b2) (hn : ∀ c ∈ C, ¬G.Adj b2 c) : False

theorem TripartiteTuran.Good.card_C_ne_one {V : Type u_1} {G : SimpleGraph V} [DecidableRel G.Adj] {A B C : Finset V} {p q r : V → ℝ} (h : Good G A B C p q r) : C.card ≠ 1

A part consisting of one vertex cannot occur.

theorem TripartiteTuran.Red_comm {V : Type u_1} {G : SimpleGraph V} [DecidableRel G.Adj] {s : Finset V} {p : V → ℝ} {Y Z : Finset V} {q r : V → ℝ} : Red s p Y q Z r ↔ Red s p Z r Y q

theorem TripartiteTuran.incomp (pi pj fi fj gi gj : ℝ) (hpi : 0 ≤ pi) (hpj : 0 ≤ pj) (h1 : ¬(pi * fi ≤ pi * fj ∧ pi * gi ≤ pi * gj)) (h2 : ¬(pj * fj ≤ pj * fi ∧ pj * gj ≤ pj * gi)) : 0 < pi ∧ 0 < pj ∧ (fi < fj ∧ gj < gi ∨ fj < fi ∧ gi < gj)

theorem TripartiteTuran.irred_pair {V : Type u_1} {G : SimpleGraph V} [DecidableRel G.Adj] {s : Finset V} {p : V → ℝ} {Y Z : Finset V} {q r : V → ℝ} (hnr : ¬Red s p Y q Z r) (hp : ∀ i ∈ s, 0 ≤ p i) {x y : V} (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y) : 0 < p x ∧ 0 < p y ∧ (nbw G x Y q < nbw G y Y q ∧ nbw G y Z r < nbw G x Z r ∨ nbw G y Y q < nbw G x Y q ∧ nbw G x Z r < nbw G y Z r)

theorem TripartiteTuran.Good.has_nbr {V : Type u_1} {G : SimpleGraph V} [DecidableRel G.Adj] [DecidableEq V] {A B C : Finset V} {p q r : V → ℝ} (h : Good G A B C p q r) (hnr : ¬Red B q C r A p) (hB2 : B.card = 2) (b : V) : b ∈ B → ∃ c ∈ C, G.Adj b c

theorem TripartiteTuran.Good.no_full_core {V : Type u_1} {G : SimpleGraph V} [DecidableRel G.Adj] [DecidableEq V] {A B C : Finset V} {p q r : V → ℝ} (h : Good G A B C p q r) {a b1 b2 c0 : V} (ha : a ∈ A) (hb1 : b1 ∈ B) (hb2 : b2 ∈ B) (hC2 : C.card = 2) (hc0 : c0 ∈ C) (hac0 : G.Adj a c0) (hf1 : G.Adj a b1) (hf2 : G.Adj a b2) (hn1 : ∃ c ∈ C, G.Adj b1 c) (hn2 : ∃ c ∈ C, G.Adj b2 c) (hrig1 : ¬(q b1 * nbw G b1 C r ≤ q b1 * nbw G b2 C r ∧ q b1 * nbw G b1 A p ≤ q b1 * nbw G b2 A p)) (hrig2 : ¬(q b2 * nbw G b2 C r ≤ q b2 * nbw G b1 C r ∧ q b2 * nbw G b2 A p ≤ q b2 * nbw G b1 A p)) : False

theorem TripartiteTuran.Good.no_full {V : Type u_1} {G : SimpleGraph V} [DecidableRel G.Adj] [DecidableEq V] {A B C : Finset V} {p q r : V → ℝ} (h : Good G A B C p q r) (hnr : ¬Red B q C r A p) (hB2 : B.card = 2) (hC2 : C.card = 2) (hbc : ∀ b ∈ B, ∃ c ∈ C, G.Adj b c) (hac : ∀ a ∈ A, ∃ c ∈ C, G.Adj a c) (a : V) : a ∈ A → ∃ b ∈ B, ¬G.Adj a b

theorem TripartiteTuran.pair_fact {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {Y : Finset V} {y1 y2 x : V} (hY : Y = {y1, y2}) (hex : ∃ y ∈ Y, G.Adj x y) (hnf : ∃ y ∈ Y, ¬G.Adj x y) : G.Adj x y1 ∧ ¬G.Adj x y2 ∨ ¬G.Adj x y1 ∧ G.Adj x y2

theorem TripartiteTuran.matching4 (p11 p12 p21 p22 : Prop) (fA1 : p11 ∧ ¬p12 ∨ ¬p11 ∧ p12) (fA2 : p21 ∧ ¬p22 ∨ ¬p21 ∧ p22) (fB1 : p11 ∧ ¬p21 ∨ ¬p11 ∧ p21) (fB2 : p12 ∧ ¬p22 ∨ ¬p12 ∧ p22) : p11 ∧ p22 ∧ ¬p12 ∧ ¬p21 ∨ p12 ∧ p21 ∧ ¬p11 ∧ ¬p22

theorem TripartiteTuran.Good.final {V : Type u_1} {G : SimpleGraph V} [DecidableRel G.Adj] [DecidableEq V] {A B C : Finset V} {p q r : V → ℝ} (h : Good G A B C p q r) (hA : ¬Red A p B q C r) (hB : ¬Red B q C r A p) (hC : ¬Red C r A p B q) (hA2 : A.card = 2) (hB2 : B.card = 2) (hC2 : C.card = 2) : False

theorem TripartiteTuran.Good.false {V : Type u_1} {G : SimpleGraph V} [DecidableRel G.Adj] [DecidableEq V] (n : ℕ) {A B C : Finset V} {p q r : V → ℝ} : A.card + B.card + C.card ≤ n → Good G A B C p q r → False

Main induction: no weighted cyclic triangle-free configuration exists.

noncomputable def TripartiteTuran.dens {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] (A B : Finset V) : ℝ

Edge density between A and B.

Equations

• TripartiteTuran.dens G A B = ↑{p ∈ A ×ˢ B | G.Adj p.1 p.2}.card / (↑A.card * ↑B.card)

theorem TripartiteTuran.dd_const {V : Type u_1} {G : SimpleGraph V} [DecidableRel G.Adj] [DecidableEq V] (A B : Finset V) (hA : A.Nonempty) (hB : B.Nonempty) : (dd G A B (fun (x : V) => 1 / ↑A.card) fun (x : V) => 1 / ↑B.card) = dens G A B

theorem TripartiteTuran.sum_const_div {V : Type u_1} (A : Finset V) (hA : A.Nonempty) : ∑ _a ∈ A, 1 / ↑A.card = 1

theorem TripartiteTuran.exists_triangle_of_mul_add {V : Type u_1} {G : SimpleGraph V} [DecidableRel G.Adj] [DecidableEq V] (A B C : Finset V) (hA : A.Nonempty) (hB : B.Nonempty) (hC : C.Nonempty) (h1 : 1 < dens G A B * dens G B C + dens G A C) (h2 : 1 < dens G B C * dens G A C + dens G A B) (h3 : 1 < dens G A C * dens G A B + dens G B C) : ∃ a ∈ A, ∃ b ∈ B, ∃ c ∈ C, G.Adj a b ∧ G.Adj b c ∧ G.Adj a c

Tripartite Turán, strong form. If αβ + γ > 1, βγ + α > 1 and γα + β > 1 for the edge densities α, β, γ between A, B, B, C, A, C, there is a triangle with one vertex in each part.

theorem TripartiteTuran.exists_triangle {V : Type u_1} {G : SimpleGraph V} [DecidableRel G.Adj] [DecidableEq V] (A B C : Finset V) (hA : A.Nonempty) (hB : B.Nonempty) (hC : C.Nonempty) (dAB : 1 / Real.goldenRatio < ↑{p ∈ A ×ˢ B | G.Adj p.1 p.2}.card / (↑A.card * ↑B.card)) (dBC : 1 / Real.goldenRatio < ↑{p ∈ B ×ˢ C | G.Adj p.1 p.2}.card / (↑B.card * ↑C.card)) (dAC : 1 / Real.goldenRatio < ↑{p ∈ A ×ˢ C | G.Adj p.1 p.2}.card / (↑A.card * ↑C.card)) : ∃ a ∈ A, ∃ b ∈ B, ∃ c ∈ C, G.Adj a b ∧ G.Adj b c ∧ G.Adj a c

A tripartite Turán theorem (Bondy–Shen–Thomassé–Thomassen 2006). If the three edge densities between A, B, C all exceed 1/φ, there is a triangle with one vertex in each part.