Counting prime edges with entropy (Lemma 4)

For each prime p, the fibres of the p-smooth part split T; on each fibre Lemma 3 applies with level v_p. Summing over primes and using the chain rule gives the edge bound.

theorem RunsOfMultiples.mem_fibre_of_prime_mul {T : Finset ℕ} (hT : ∀ m ∈ T, 0 < m) {p q : ℕ} (hp : Nat.Prime p) (hqp : q ≤ p) {m : ℕ} (hm : m ∈ T) (hpm : p * m ∈ T) : p * m ∈ {x ∈ T | key q x = key q m}

Per prime: if p * m ∈ T for all m ∈ G ⊆ T, then the fibrewise Lemma 3 bounds hold.

theorem RunsOfMultiples.D_ge_log_two (T : Finset ℕ) (hT : ∀ m ∈ T, 0 < m) {p : ℕ} (hp : Nat.Prime p) (G : Finset ℕ) (hGT : G ⊆ T) (hG : ∀ m ∈ G, p * m ∈ T) : Real.log 2 / 2 * ↑G.card ≤ D T p

D T p ≥ (log 2 / 2) |G| whenever multiplication by the prime p maps G ⊆ T into T.

theorem RunsOfMultiples.edge_bound (T : Finset ℕ) (hT : ∀ m ∈ T, 0 < m) (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) (E : ℕ → Finset ℕ) (hET : ∀ p ∈ P, E p ⊆ T) (hE : ∀ p ∈ P, ∀ m ∈ E p, p * m ∈ T) : Real.log 2 / 2 * ∑ p ∈ P, ↑(E p).card ≤ ↑T.card * Real.log ↑T.card

Lemma 4 (edge count).