OAI/Combinatorics/HadwigerCounterexample/GreedyExposures.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HadwigerCounterexample.price line 13
2. theorem OAI.HadwigerCounterexample.tax_comp line 16
3. theorem OAI.HadwigerCounterexample.price_drop line 25
4. theorem OAI.HadwigerCounterexample.union_arrange line 31
5. theorem OAI.HadwigerCounterexample.grow line 34
6. theorem OAI.HadwigerCounterexample.greedy_expose line 67

   Source documentation

   Dyadic selection if potential is strictly too low to sustain all bad tail deficit ratios

   private theorem greedy_expose (f : I→Ambient p N) (S : Cov p N) (W : Finset I)
       (b m : ℕ) (hW : W.card=2^m*b)
       (hg : 4*(W.card*price f S W+tax p S (arrange p f W)) < W.card*m) :
       ∃ E R : Finset I, W=E∪R ∧ Disjoint E R ∧ b≤R.card ∧
         let s' := S⊔arrange p f E
   …

   Mentions: OAI.HadwigerCounterexample.Ambient, OAI.HadwigerCounterexample.Cov, OAI.HadwigerCounterexample.price, OAI.HadwigerCounterexample.tax, OAI.HadwigerCounterexample.arrange

7. theorem OAI.HadwigerCounterexample.sum_charge_sign line 103
8. theorem OAI.HadwigerCounterexample.arrange_bound line 120
9. theorem OAI.HadwigerCounterexample.sparse_covered line 125