OAI/Combinatorics/CliqueFree/Main.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CliqueFreeLog.sum_degrees_real line 15
2. theorem OAI.CliqueFreeLog.logarithmic_independence_bound line 22

   Source documentation

   The logarithmic independence bound for ordinary clique exclusion and the graph's own average degree, with a constant uniform in graph size and average degree.

   Distinct definitions of this name: ComparatorChallenges/CliqueFreeLog.lean:11 (same statement text; different proof or body). Qualify references as OAI.CliqueFreeLog.logarithmic_independence_bound@path.

   theorem logarithmic_independence_bound (r : ℕ) (hr : 4 ≤ r) :
       ∃ c : ℝ, 0 < c ∧
         ∀ {V : Type} [Fintype V] (G : SimpleGraph V),
           G.CliqueFree r → 2 ≤ averageDegree G →
           c * (Fintype.card V : ℝ) * Real.log (averageDegree G) / averageDegree G ≤
             (G.indepNum : ℝ) := by
   …

   Mentions: OAI.CliqueFreeLog.averageDegree