OAI/Combinatorics/CliqueFree/DisjointCross.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CliqueFreeIndependence.WeightedGraph.log_multiplier_le line 19

   Source documentation

   A logarithm estimate with log 2 ≤ 1 already applied.

   lemma log_multiplier_le (k : ℕ) {x : ℝ} (hx : 1 ≤ x) :
       Real.log (1 + Real.exp (4*x) * multiplierBound k (Real.exp (-8*x))) ≤
         (5 + 10*(k:ℝ) + (k:ℝ)^2)*x := by
   …

   Mentions: OAI.CliqueFreeIndependence.WeightedGraph.multiplierBound

2. lemma OAI.CliqueFreeIndependence.WeightedGraph.cross_error_le line 50
3. lemma OAI.CliqueFreeIndependence.WeightedGraph.optimizer_cross_disjoint_moderate line 71
4. lemma OAI.CliqueFreeIndependence.WeightedGraph.optimizer_cross_disjoint line 108