OAI/Combinatorics/HadwigerCounterexample/ConstructionScales.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Construction Scales

  1. theorem OAI.HadwigerCounterexample.card_full line 12
  2. theorem OAI.HadwigerCounterexample.full_linear line 19
  3. theorem OAI.HadwigerCounterexample.unit_size line 32
  4. theorem OAI.HadwigerCounterexample.have_budget line 48

    Source documentation

    Fixed linear and constant expenses become any fixed small fraction of N.

    theorem have_budget {δ : ℝ} (hd : 0 < δ) (a b : ℝ) (hb : 0 ≤ b) :
    ∀ᶠ M : ℕ in atTop, ∀ n : ℕ, 1 ≤ n → a*n+b ≤ δ*(M*n : ℕ) := by
…
  5. theorem OAI.HadwigerCounterexample.columns_budget line 59
  6. theorem OAI.HadwigerCounterexample.raw_ready line 69