OAI/Combinatorics/CliqueFree/Packing.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

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

   Source documentation

   Greedy disjoint-neighborhood packing, with a subprobability lottery. The additional zero outcome is inserted only at the end.

   lemma neighborhood_packing (G : SimpleGraph V) {w : V → ℝ} (hw : ∀ v, 0 < w v)
       (A : Finset V) {s η b B : ℝ} (hs : 0 < s) (hη : 0 < η) (hb : 0 ≤ b)
       (hB : 2 ≤ B) (hbig : 2/η*b ≤ B) (_hAs : mass w A ≤ s)
       (hlocal : ∀ (R : Finset V), R ⊆ A → ∀ v ∈ R,
         η*s < mass w (R ∩ neighbors G v) →
         ∃ L : Law (V → ℝ), IsProb L ∧ BoundedOn L (R ∩ neighbors G v) b ∧
           (∀ u, expect L (fun m ↦ m u) = if u ∈ R ∩ neighbors G v then 1 else 0) ∧
           expectedEdges G w L ≤ η * (mass w (R ∩ neighbors G v))^2) :
       ∃ L : Law (V → ℝ), Positive L ∧ total L ≤ 1/2+mass w A/(2*s) ∧
         BoundedOn L A B ∧
         (∀ u, expect L (fun m ↦ m u) = if u ∈ A then 1 else 0) ∧
         expectedEdges G w L ≤ 2*η*s*mass w A := by
   …

   Mentions: OAI.CliqueFreeIndependence.WeightedGraph.mass, OAI.CliqueFreeIndependence.WeightedGraph.neighbors, OAI.CliqueFreeIndependence.WeightedGraph.BoundedOn, OAI.CliqueFreeIndependence.WeightedGraph.expectedEdges