OAI/Combinatorics/HadwigerCounterexample/PolynomialRankBounds.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HadwigerCounterexample.mpMask line 13
2. theorem OAI.HadwigerCounterexample.rank_mask line 15
3. theorem OAI.HadwigerCounterexample.choose_draws line 38
4. theorem OAI.HadwigerCounterexample.simultaneous_czeros line 59

   Source documentation

   Here T counts k^2+1 draws, union bound uses crude T^2. Even repeats give the event.

   theorem simultaneous_czeros (P : Mat A A) (k : ℕ)
       (w : Wgt A) (hw : IsLaw w) (hK : 1+P.rank ≤ k)
       (h : ∀ x,P x x=0) :
       1 ≤ ((k:ℝ)^2+1)^2 * pr (pairW w w) (fun x => P x.1 x.2=0 ∧ P x.2 x.1=0) := by
   …

   Mentions: OAI.HadwigerCounterexample.Mat, OAI.HadwigerCounterexample.Wgt, OAI.HadwigerCounterexample.IsLaw, OAI.HadwigerCounterexample.pr, OAI.HadwigerCounterexample.pairW