Transferring multiplicative blocks to every large cardinality

Positive-density blocks with controlled size produce the sharp lower asymptotic order.

theorem RunsOfMultiples.lower_bound_of_block {δ C₂ : ℝ} (hδ : 0 < δ) (hC₂ : 0 < C₂) (hblock : ∀ (y : ℕ), 2 ≤ y → ∃ (B : Finset ℕ) (G : Finset ℕ), (∀ a ∈ B, 0 < a) ∧ G ⊆ B ∧ (∀ a ∈ G, ∀ (j : ℕ), 1 ≤ j → j ≤ y → j * a ∈ B) ∧ 0 < B.card ∧ δ * ↑B.card ≤ ↑G.card ∧ ↑B.card ≤ Real.exp (C₂ * (↑y / Real.log ↑y))) : ∃ (c : ℝ), 0 < c ∧ ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∃ (S : Finset ℕ), (∀ a ∈ S, 0 < a) ∧ S.card = n ∧ c * ↑n * Real.log ↑n * Real.log (Real.log ↑n) ≤ ↑(∑ a ∈ S, kVal S a)

A positive-density block with exponential size bounds yields the sharp lower order.