GoodCellTargets.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Shifted cell indices and target sums

def OAI.Ostmann.cellDifferences line 11
Source documentation
The nonnegative differences of a set of cell indices from its first index.
```
def cellDifferences (I : Finset ℕ) (a : ℕ) : Finset ℕ :=
…
```
theorem OAI.Ostmann.cellDifferences_card line 14

theorem OAI.Ostmann.dense_cell_exact_sum line 25

Source documentation

A dense interval set realizes every interior target in the appropriate residue class, with an exact prescribed number of cell labels.

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

Mentions: OAI.Ostmann.cellDifferences

theorem OAI.Ostmann.dense_difference_gcd_bound line 62

Source documentation

Density bounds the lattice spacing of the cell differences.

theorem dense_difference_gcd_bound (A : Finset ℕ) (s : ℕ) (hs : 0 < s)
    (hend : s ∈ A) (hbound : ∀ a ∈ A, a ≤ s) (δ : ℝ)
    (hdensity : δ * s + 1 ≤ A.card) :
    δ * (A.gcd id : ℕ) ≤ 1 := by
…