OAI/Combinatorics/HadwigerCounterexample/SumRankBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HadwigerCounterexample.draws line 13
2. theorem OAI.HadwigerCounterexample.draws_law line 15
3. def OAI.HadwigerCounterexample.refresh line 18
4. theorem OAI.HadwigerCounterexample.fresh_avg line 21
5. theorem OAI.HadwigerCounterexample.draws_all line 46
6. theorem OAI.HadwigerCounterexample.arrange_fresh line 63
7. theorem OAI.HadwigerCounterexample.no_cover_rank line 75

   Source documentation

   With s=2^m*(2b), not requiring s itself to be a power of two.

   theorem no_cover_rank (p : Shape) {N} (f : A→ Ambient p N) (w : Wgt A)
       (hw : IsLaw w) (m b r : ℕ) (hb : 1 ≤ b) (hr : 16*r<m)
       (hf : ∀ i,epoch p (f i)≤ r)
       (c : ℝ) (hc : 0 ≤ c)
       (he : ∀ S : Cov p N,(∀ i, cdSign p S i ≤ r*(2^m*(2*b))) →
         pr w (fun i => covered p S (f i)) ≤ c) :
       let s := 2^m*(2*b)
   …

   Mentions: OAI.HadwigerCounterexample.Shape, OAI.HadwigerCounterexample.Ambient, OAI.HadwigerCounterexample.Wgt, OAI.HadwigerCounterexample.IsLaw, OAI.HadwigerCounterexample.epoch, OAI.HadwigerCounterexample.Cov, OAI.HadwigerCounterexample.cdSign, OAI.HadwigerCounterexample.pr, OAI.HadwigerCounterexample.covered