IntegerSumsetCover.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Lifting cyclic covering to exact integer sums

The bounded cyclic word can be padded with zero and the upper endpoint. This is the finite, exact version of the good-cell interior sumset argument.

theorem OAI.Ostmann.integer_interval_sum_cover line 19

Source documentation

A cyclic cover by r summands covers the interior interval with any prescribed longer number of summands.

theorem integer_interval_sum_cover (A : Finset ℕ) (s r n : ℕ)
    (hs : 0 < s) (h0 : 0 ∈ A) (hend : s ∈ A)
    (hbound : ∀ a ∈ A, a ≤ s) (hrn : r ≤ n)
    (hcover : ∀ x : ZMod s, ∃ f : Fin r → ℕ,
      (∀ i, f i ∈ A) ∧ ∑ i, (f i : ZMod s) = x)
    (t : ℕ) (hlo : r * s ≤ t) (hhi : t ≤ (n - r) * s) :
    ∃ w : List ℕ, w.length = n ∧ (∀ a ∈ w, a ∈ A) ∧ w.sum = t := by
…

theorem OAI.Ostmann.lift_cyclic_sum_cover line 57

Source documentation

The tuple version of the cyclic covering theorem lifts through the actual residue image of a finite set of nonnegative integers.

theorem lift_cyclic_sum_cover (A : Finset ℕ) (s r : ℕ)
    (hcover : ∀ x : ZMod s, ∃ f : Fin r → ZMod s,
      (∀ i, f i ∈ A.image (fun a : ℕ => (a : ZMod s))) ∧ ∑ i, f i = x) :
    ∀ x : ZMod s, ∃ f : Fin r → ℕ,
      (∀ i, f i ∈ A) ∧ ∑ i, (f i : ZMod s) = x := by
…