Replicating finite multiplicative blocks

Disjoint dilates and padding preserve cardinality and a quantitative lower bound on runs.

Replication of a block

theorem RunsOfMultiples.pow_mul_inj {M j j' a a' : ℕ} (ha : 0 < a) (ha' : 0 < a') (haM : a < M) (haM' : a' < M) (h : M ^ j * a = M ^ j' * a') : j = j' ∧ a = a'

theorem RunsOfMultiples.replicate (B G : Finset ℕ) (y n : ℕ) (hB : ∀ a ∈ B, 0 < a) (hGB : G ⊆ B) (hG : ∀ a ∈ G, ∀ (j : ℕ), 1 ≤ j → j ≤ y → j * a ∈ B) : ∃ (S : Finset ℕ), (∀ a ∈ S, 0 < a) ∧ S.card = n ∧ n / B.card * G.card * (y + 1) ≤ ∑ a ∈ S, kVal S a

Replication: from a block B with a subset G whose first y multiples lie in B, build an n-element set of positive integers whose kVal-sum is at least ⌊n / |B|⌋ · |G| · (y + 1).