OAI/Combinatorics/Ramsey/CycleClique/Construction/FullLargeClique.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The quantitative clique bound of manuscript Theorem clq:bound.

  1. theorem OAI.CycleClique.Construction.dense_layer_forces_cycle line 11
  2. theorem OAI.CycleClique.Construction.large_clique_bounds line 31

    Source documentation

    Manuscript Theorem clq:bound, with expansion and exact forbidden cycle as hypotheses.

    theorem large_clique_bounds {V : Type*} [Fintype V] [DecidableEq V] {G : SimpleGraph V}
    {k a : ℕ} (hk : 3 ≤ k) (ha : 2 ≤ a) (hak : a ≤ k)
    (hcard : Fintype.card V = k * a + 1) (hI : IndependenceBound G a)
    (hcycle : ¬ HasCycle G (k + 1))
    (hexpand : ∀ I : Finset V, G.IsIndepSet (I : Set V) → I.Nonempty →
      k * I.card + 1 ≤ (closedNeighborhood G I).card) :
    max 3 (k / 2) ≤ G.cliqueNum ∧ G.cliqueNum ≤ k := by
…

    Mentions: OAI.CycleClique.Construction.IndependenceBound, OAI.CycleClique.Construction.HasCycle, OAI.CycleClique.Construction.closedNeighborhood