OAI/Combinatorics/CliqueFree/MaxDegree.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CliqueFreeIndependence.WeightedGraph.log_le_one_add_quarter line 18
2. lemma OAI.CliqueFreeIndependence.WeightedGraph.neighborMass_const line 29
3. lemma OAI.CliqueFreeIndependence.WeightedGraph.edgeMass_const_le line 33
4. lemma OAI.CliqueFreeIndependence.WeightedGraph.potential_const_lower line 48
5. lemma OAI.CliqueFreeIndependence.WeightedGraph.maximum_degree_independence line 70

   Source documentation

   The quantitative maximum-degree independence bound.

   lemma maximum_degree_independence (k : ℕ) {B Δ : ℝ} (hB : 0 ≤ B) (hΔ : 3 ≤ Δ)
       (htri : ∀ {U : Type u} [Fintype U] (H : SimpleGraph U) (w : U → ℝ),
         IsOptimizer H w → H.CliqueFree (k+2) → triangleMass H w ≤ B * edgeMass H w)
       (G : SimpleGraph V) (hf : G.CliqueFree (k+2)) (hdeg : ∀ v, (G.degree v : ℝ) ≤ Δ) :
       (Fintype.card V : ℝ)*Real.log Δ/(4*(3+3*B/2)*Δ) ≤ (G.indepNum : ℝ) := by
   …

   Mentions: OAI.CliqueFreeIndependence.WeightedGraph.IsOptimizer, OAI.CliqueFreeIndependence.WeightedGraph.triangleMass, OAI.CliqueFreeIndependence.WeightedGraph.edgeMass

6. lemma OAI.CliqueFreeIndependence.WeightedGraph.indepNum_induce_le line 87
7. lemma OAI.CliqueFreeIndependence.WeightedGraph.degree_cutoff_card line 94