OAI/Combinatorics/CliqueFree/IndependentSet.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CliqueFreeIndependence.WeightedGraph.exists_optimizer_triangle_bound line 20
2. lemma OAI.CliqueFreeIndependence.WeightedGraph.exists_cheap_vertex line 28
3. lemma OAI.CliqueFreeIndependence.WeightedGraph.degree_induce_le line 69
4. lemma OAI.CliqueFreeIndependence.WeightedGraph.indepSet_image_induce line 82
5. lemma OAI.CliqueFreeIndependence.WeightedGraph.indepSet_insert_induce line 92
6. lemma OAI.CliqueFreeIndependence.WeightedGraph.maximum_degree_potential_bound line 120

   Source documentation

   The maximum-degree induction controls the original variational functional, not a surrogate objective or a conditional independence bound.

   lemma maximum_degree_potential_bound (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 : ℝ) ≤ Δ) :
       ∃ I : Finset V, G.IsIndepSet (I : Set V) ∧
         ∀ q : V → ℝ, (∀ v, 0 ≤ q v) →
           potential G q ≤ ((3+3*B/2)*Real.log Δ) * (I.card : ℝ) := by
   …

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