OAI/Combinatorics/CliqueFree/VertexSplitting.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CliqueFreeIndependence.WeightedGraph.splittingConstant line 20
2. lemma OAI.CliqueFreeIndependence.WeightedGraph.splitting_error_le line 23
3. lemma OAI.CliqueFreeIndependence.WeightedGraph.weighted_splitting line 50

   Source documentation

   Weighted vertex splitting with explicit constants.

   lemma weighted_splitting {G : SimpleGraph V} [Nonempty (EdgeState G)] {w : V → ℝ}
       (hw : ∀ u, 0 < w u) {C x : ℝ} (hC : 1 ≤ C) (hCross : CrossBound G w C)
       (hx : 32 ≤ x) (hc : ∀ u v, G.Adj u v → 1 / x ≤ commonMass G w u v)
       (hL : ∀ u, neighborMass G w u ≤ Real.exp x) :
       ∃ H : SimpleGraph (EdgeState G), EdgeProjection H G EdgeState.src ∧
         (∀ z, neighborMass H (w ∘ EdgeState.src) z ≤ Real.exp (Real.sqrt x)) ∧
         (1 - splittingConstant C * (Real.log x / Real.sqrt x)) * triangleMass G w ≤
           triangleMass H (w ∘ EdgeState.src) := by
   …

   Mentions: OAI.CliqueFreeIndependence.WeightedGraph.EdgeState, OAI.CliqueFreeIndependence.WeightedGraph.CrossBound, OAI.CliqueFreeIndependence.WeightedGraph.commonMass, OAI.CliqueFreeIndependence.WeightedGraph.neighborMass, OAI.CliqueFreeIndependence.WeightedGraph.EdgeProjection, OAI.CliqueFreeIndependence.WeightedGraph.EdgeState.src, OAI.CliqueFreeIndependence.WeightedGraph.splittingConstant, OAI.CliqueFreeIndependence.WeightedGraph.triangleMass