The one-step entropy lemma

If G ⊆ R and multiplication by q maps G into R, raising a "level" function by one, then the counting entropy of the level on R is at least (|G|/2) log (2|R|/|G|).

theorem RunsOfMultiples.mul_log_div_mono {a b N : ℝ} (ha : 0 < a) (hab : a ≤ b) (hbN : b * Real.exp 1 ≤ N) : a * Real.log (N / a) ≤ b * Real.log (N / b)

x ↦ x log (N/x) is monotone on (0, N/e].

theorem RunsOfMultiples.mul_log_div_le {x N : ℝ} (hx : 0 < x) (hN : 0 < N) : x * Real.log (N / x) ≤ N * Real.exp (-1)

x log (N/x) ≤ N/e.

theorem RunsOfMultiples.le_mul_log_div_sub {δ N : ℝ} (hδ : 0 ≤ δ) (hδN : δ < N) : δ ≤ N * Real.log (N / (N - δ))

δ ≤ N log (N / (N - δ)) for 0 ≤ δ < N.

theorem RunsOfMultiples.ent_ge_of_shift (R G : Finset ℕ) (lev : ℕ → ℕ) (q : ℕ) (hq : 0 < q) (hGR : G ⊆ R) (hmap : ∀ m ∈ G, q * m ∈ R ∧ lev (q * m) = lev m + 1) (hG : G.Nonempty) : ↑G.card / 2 * Real.log (2 * ↑R.card / ↑G.card) ≤ ent R lev

Lemma 3 (one-step entropy).

theorem RunsOfMultiples.ent_ge_log_two (R G : Finset ℕ) (lev : ℕ → ℕ) (q : ℕ) (hq : 0 < q) (hGR : G ⊆ R) (hmap : ∀ m ∈ G, q * m ∈ R ∧ lev (q * m) = lev m + 1) : Real.log 2 / 2 * ↑G.card ≤ ent R lev

Weak form: every shifted element contributes log 2 / 2.

theorem RunsOfMultiples.ent_ge_sparse (R G : Finset ℕ) (lev : ℕ → ℕ) (q : ℕ) (hq : 0 < q) (hGR : G ⊆ R) (hmap : ∀ m ∈ G, q * m ∈ R ∧ lev (q * m) = lev m + 1) (hsparse : ↑G.card * √↑q ≤ ↑R.card) : ↑G.card / 4 * Real.log ↑q ≤ ent R lev

Sparse form: if |G| √q ≤ |R| then the entropy is at least (|G|/4) log q.