OAI/Combinatorics/CliqueFree/CrossBound.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CliqueFreeIndependence.WeightedGraph.bool_point_count line 20
2. lemma OAI.CliqueFreeIndependence.WeightedGraph.bool_pair_count line 35
3. lemma OAI.CliqueFreeIndependence.WeightedGraph.crossMass_colored line 54
4. lemma OAI.CliqueFreeIndependence.WeightedGraph.sum_colored_cross line 77
5. theorem OAI.CliqueFreeIndependence.WeightedGraph.optimizer_cross_bound line 96

   Source documentation

   Full optimizer cross mass, including overlapping sets, with an explicit constant.

   theorem optimizer_cross_bound (k : ℕ) (G : SimpleGraph V) {w : V → ℝ}
       (hw : IsOptimizer G w) (hfree : G.CliqueFree (k+2)) :
       CrossBound G w (16*((k:ℝ)+2)^2) := by
   …

   Mentions: OAI.CliqueFreeIndependence.WeightedGraph.IsOptimizer, OAI.CliqueFreeIndependence.WeightedGraph.CrossBound