OAI/Combinatorics/HadwigerCounterexample/EntropyContainers.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HadwigerCounterexample.avg_reached line 15
2. theorem OAI.HadwigerCounterexample.closed_carried line 32
3. theorem OAI.HadwigerCounterexample.containers line 40

   Source documentation

   Cover the conflict-independent sets in R by a small family of terminal sets.

   theorem containers {ok : Set (Wgt α)} (hcomp : IsCompact ok) (hok : ∀ w ∈ ok, IsLaw w)
       (hmid : ∀ w ∈ ok, ∀ v ∈ ok, midLaw w v ∈ ok) (rel : α → α → Prop)
       {e : ℝ} (he : 0 < e) (R : Finset α)
       (hsat : ∀ w ∈ ok, carried w (· ∈ R) →
         e ≤ pr (pairW w w) (fun x => rel x.1 x.2))
       (L : ℕ) (hL : ∀ w ∈ ok, carried w (· ∈ R) →
         0 < negEnt w + L * (e * Real.log 2)) :
       ∃ C : Finset (Finset α),
         C.card ≤ (R.card + 1)^L ∧
         (∀ r ∈ C, r ⊆ R ∧ ¬∃ w ∈ ok, carried w (· ∈ r)) ∧
         ∀ I : Finset α, I ⊆ R → (∀ v ∈ I, ∀ u ∈ I, ¬rel v u) →
           ∃ r ∈ C, I ⊆ r := by
   …

   Mentions: OAI.HadwigerCounterexample.Wgt, OAI.HadwigerCounterexample.IsLaw, OAI.HadwigerCounterexample.midLaw, OAI.HadwigerCounterexample.carried, OAI.HadwigerCounterexample.pr, OAI.HadwigerCounterexample.pairW, OAI.HadwigerCounterexample.negEnt