GoodCellSums.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Exact interior sums of dense sets of cell differences

The covering length depends only on the density. Every admissible multiple of the actual gcd in the interior interval has an ordered representation.

theorem OAI.Ostmann.dense_difference_sum_cover line 17

Source documentation

Uniform exact covering of the interior by sums of a dense set of differences.

theorem dense_difference_sum_cover (δ : ℝ) (hδ : 0 < δ) :
    ∃ r : ℕ, 0 < r ∧ ∀ (A : Finset ℕ) (s : ℕ),
      0 < s → 0 ∈ A → s ∈ A → (∀ a ∈ A, a ≤ s) →
      δ * s + 1 ≤ A.card → ∀ n : ℕ, r ≤ n → ∀ t : ℕ,
      A.gcd id ∣ t → r * s ≤ t → t ≤ (n - r) * s →
      ∃ w : List ℕ, w.length = n ∧ (∀ a ∈ w, a ∈ A) ∧ w.sum = t := by
…