OAI/Combinatorics/CliqueFree/SparseMultipliers.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CliqueFreeIndependence.WeightedGraph.multiplierBound line 18

   Source documentation

   The bound b_(k+2)(ε), indexed by the excess clique size.

   noncomputable def multiplierBound (k : ℕ) (ε : ℝ) : ℝ := 2^((k+2)*k) / ε^k

2. lemma OAI.CliqueFreeIndependence.WeightedGraph.multiplierBound_pos line 20
3. lemma OAI.CliqueFreeIndependence.WeightedGraph.multiplierBound_ge_one line 24
4. lemma OAI.CliqueFreeIndependence.WeightedGraph.multiplierBound_step line 30
5. lemma OAI.CliqueFreeIndependence.WeightedGraph.sparse_multipliers_on line 40