OAI/Combinatorics/HadwigerCounterexample/ExponentialGraphTransfer.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HadwigerCounterexample.ord line 12
2. theorem OAI.HadwigerCounterexample.cast_ord line 13
3. theorem OAI.HadwigerCounterexample.tendsto_ord line 19
4. theorem OAI.HadwigerCounterexample.transfer_scales line 32

   Source documentation

   Raw supersaturation ⇒ existence for the sampled order. Takes any fixed polynomial bit-count bound of degree two for the raw unit space. In particular the eventual N-bound is independent of every law and graph.

   theorem transfer_scales {g : ℕ} (hg : 0 < g) {B : ℝ} (hB : 0 ≤ B) :
       ∀ᶠ N : ℕ in atTop, ∀ (A : Type) [Fintype A] [Nonempty A]
         (H : Holes A) (μ : Wgt A), IsLaw μ →
         (Fintype.card (A × A) : ℝ) ≤ bp (B * (N:ℝ)^2) →
         (∀ w : Wgt (A × A), IsLaw w → pairCaps μ (bp 1000) (bp (4000*g*N)) w →
           carried w H.unit → bp (-100*g*N) ≤ pr (pairW w w) (fun x => H.conflict x.1 x.2)) →
         ∃ x : Fin (ord g N) → A,
           (H.graph x).indepNum ≤ 2 ∧
           (connectedMatchingNumber (H.graph x) : ℚ) < (ord g N : ℚ)/100 := by
   …

   Mentions: OAI.HadwigerCounterexample.Holes, OAI.HadwigerCounterexample.Wgt, OAI.HadwigerCounterexample.IsLaw, OAI.HadwigerCounterexample.bp, OAI.HadwigerCounterexample.pairCaps, OAI.HadwigerCounterexample.carried, OAI.HadwigerCounterexample.pr, OAI.HadwigerCounterexample.pairW, OAI.HadwigerCounterexample.ord