CyclicSumsetCover.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

A bounded number of sums in a dense generating set

The good-cell construction needs a uniform covering length in a finite cyclic group. The elementary small-doubling theorem already in Mathlib supplies this without any additional published-input hypothesis. Constants need not be optimal here.

theorem OAI.Ostmann.small_doubling_cover line 22
theorem OAI.Ostmann.product_growth_or_cover line 52
theorem OAI.Ostmann.dyadic_product_growth line 59

theorem OAI.Ostmann.exists_uniform_product_cover line 93

Source documentation

A positive-density generating set containing the identity covers its finite group in a number of products depending only on the density.

private theorem exists_uniform_product_cover (δ : ℝ) (hδ : 0 < δ) :
    ∃ r : ℕ, 0 < r ∧ ∀ (G : Type*) [Group G] [Fintype G] [DecidableEq G]
      (A : Finset G), 1 ∈ A → Subgroup.closure (A : Set G) = ⊤ →
      δ * Fintype.card G ≤ A.card → A ^ r = Finset.univ := by
…

theorem OAI.Ostmann.exists_uniform_cyclic_sum_cover line 114

Source documentation

Uniform cyclic covering, expressed as an ordered tuple of summands.

theorem exists_uniform_cyclic_sum_cover (δ : ℝ) (hδ : 0 < δ) :
    ∃ r : ℕ, 0 < r ∧ ∀ (q : ℕ) [NeZero q] (S : Finset (ZMod q)),
      0 ∈ S → AddSubgroup.closure (S : Set (ZMod q)) = ⊤ →
      δ * q ≤ S.card → ∀ x : ZMod q,
      ∃ f : Fin r → ZMod q, (∀ i, f i ∈ S) ∧ ∑ i, f i = x := by
…