OAI/Combinatorics/HadwigerCounterexample/InitialPartitionExistence.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HadwigerCounterexample.PreparationParameters.born line 17
2. structure OAI.HadwigerCounterexample.PreparationParameters.entry line 25
3. theorem OAI.HadwigerCounterexample.PreparationParameters.stamp line 32

   Source documentation

   combines early h & M choices assuming row/selector bounds supplied.

   theorem stamp (g : ℕ) (q : PreparationParameters)
       (hq : q.allows) (hd : 0 < q.D) (hf : (q.D:ℝ)+q.ζ ≤ (q.ζ-q.ζ/4)*q.e)
       (hk : q.k≤ q.d) (hg : q.spJoint+1 ≤0.49*q.k)
       (hu : 3*q.d+2*q.e+2 ≤ q.u) :
       ∀ᶠ h : ℕ in atTop,∀ p:Shape,p.g=g→p.h=h →
       Odd p.g → 3≤p.g → 1≤p.j → 1≤p.r → (q.B:ℝ)<bp ((p.b:ℝ)-2*p.j) →
       8*q.D <p.g*p.g → (∃ d_:ℕ,4*q.D≤p.g*d_∧2*screenRank p q.e+1 ≤ ((p.g-1)/2)*(p.g-d_)*p.r) →
       ∀ᶠ M : ℕ in atTop, q.entry p M := by
   …

   Mentions: OAI.HadwigerCounterexample.PreparationParameters, OAI.HadwigerCounterexample.Shape, OAI.HadwigerCounterexample.bp, OAI.HadwigerCounterexample.screenRank