Theorems · Theorem · combinatorics

SimpleGraph.triangle_counting

∀ {α : Type u_1} (G : SimpleGraph α) [inst : DecidableRel G.Adj] {ε : ℝ} {s t u : Finset α} [inst_1 : DecidableEq α]
  [inst_2 : Fintype α],
  2 * ε ≤ ↑(G.edgeDensity s t) →
    G.IsUniform ε s t →
      Disjoint s t →
        2 * ε ≤ ↑(G.edgeDensity s u) →
          G.IsUniform ε s u →
            Disjoint s u →
              2 * ε ≤ ↑(G.edgeDensity t u) →
                G.IsUniform ε t u →
                  Disjoint t u → (1 - 2 * ε) * ε ^ 3 * ↑s.card * ↑t.card * ↑u.card ≤ ↑(G.cliqueFinset 3).card

The Triangle Counting Lemma. If G is a graph and s, t, u are disjoint sets of vertices such that each pair is ε-uniform and 2 * ε-dense, then G contains at least (1 - 2 * ε) * ε ^ 3 * |s| * |t| * |u| triangles.

Defined in

Mathlib.Combinatorics.SimpleGraph.Triangle.Counting

Cited by

0 results in Mathlib

Foundations

Depth 112 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableRelDecidableEqFintype