Counting entropy along the prime factorisation

For a finite set R and a function f, ent R f = ∑_{m ∈ R} log (|R| / |fibre of m|); this is |R| times the Shannon entropy of f(X) for X uniform on R.

key t m records the exponents of the primes < t in m (the t-smooth part of m). D T t is |T| times the conditional entropy of v_t(X) given key t X; the chain rule ∑_{t < B} D T t = |T| log |T| is sum_D.

noncomputable def RunsOfMultiples.ent {β : Type u_1} [DecidableEq β] (R : Finset ℕ) (f : ℕ → β) : ℝ

Counting entropy: |R| times the entropy of f(X), X uniform on R.

Equations

• RunsOfMultiples.ent R f = ∑ m ∈ R, Real.log (↑R.card / ↑{x ∈ R | f x = f m}.card)

theorem RunsOfMultiples.fibre_card_pos {β : Type u_1} [DecidableEq β] {R : Finset ℕ} {f : ℕ → β} {m : ℕ} (hm : m ∈ R) : 0 < {x ∈ R | f x = f m}.card

theorem RunsOfMultiples.fibre_card_le {β : Type u_1} [DecidableEq β] (R : Finset ℕ) (f : ℕ → β) (m : ℕ) : {x ∈ R | f x = f m}.card ≤ R.card

theorem RunsOfMultiples.log_card_div_fibre_nonneg {β : Type u_1} [DecidableEq β] {R : Finset ℕ} {f : ℕ → β} {m : ℕ} (hm : m ∈ R) : 0 ≤ Real.log (↑R.card / ↑{x ∈ R | f x = f m}.card)

theorem RunsOfMultiples.ent_nonneg {β : Type u_1} [DecidableEq β] (R : Finset ℕ) (f : ℕ → β) : 0 ≤ ent R f

noncomputable def RunsOfMultiples.key (t m : ℕ) : ℕ →₀ ℕ

The exponents of the primes < t in m.

Equations

• RunsOfMultiples.key t m = Finsupp.filter (fun (x : ℕ) => x < t) m.factorization

theorem RunsOfMultiples.key_apply (t m p : ℕ) : (key t m) p = if p < t then m.factorization p else 0

theorem RunsOfMultiples.key_zero (m : ℕ) : key 0 m = 0

theorem RunsOfMultiples.key_succ_eq_iff (t m m' : ℕ) : key (t + 1) m = key (t + 1) m' ↔ key t m = key t m' ∧ m.factorization t = m'.factorization t

theorem RunsOfMultiples.key_eq_factorization {t m : ℕ} (hm : ∀ p ∈ m.primeFactors, p < t) : key t m = m.factorization

theorem RunsOfMultiples.key_prime_mul {t p m : ℕ} (hp : Nat.Prime p) (htp : t ≤ p) (hm : m ≠ 0) : key t (p * m) = key t m

Multiplying by a prime p ≥ t does not change the t-smooth part.

theorem RunsOfMultiples.factorization_prime_mul_self {p m : ℕ} (hp : Nat.Prime p) (hm : m ≠ 0) : (p * m).factorization p = m.factorization p + 1

noncomputable def RunsOfMultiples.D (T : Finset ℕ) (t : ℕ) : ℝ

D T t: |T| times the conditional entropy of v_t(X) given the t-smooth part of X.

Equations

• RunsOfMultiples.D T t = ∑ c ∈ Finset.image (RunsOfMultiples.key t) T, RunsOfMultiples.ent ({m ∈ T | RunsOfMultiples.key t m = c}) fun (m : ℕ) => m.factorization t

theorem RunsOfMultiples.D_nonneg (T : Finset ℕ) (t : ℕ) : 0 ≤ D T t

theorem RunsOfMultiples.D_eq (T : Finset ℕ) (t : ℕ) : D T t = ent T (key (t + 1)) - ent T (key t)

Regrouping: D T t is the increase of ent T (key ·) from t to t + 1.

theorem RunsOfMultiples.ent_key_zero (T : Finset ℕ) : ent T (key 0) = 0

theorem RunsOfMultiples.ent_key_large (T : Finset ℕ) (hT : ∀ m ∈ T, 0 < m) {B : ℕ} (hB : ∀ m ∈ T, m < B) : ent T (key B) = ↑T.card * Real.log ↑T.card

theorem RunsOfMultiples.sum_D (T : Finset ℕ) (hT : ∀ m ∈ T, 0 < m) {B : ℕ} (hB : ∀ m ∈ T, m < B) : ∑ t ∈ Finset.range B, D T t = ↑T.card * Real.log ↑T.card

Chain rule: the conditional entropies along all primes add up to |T| log |T|.

theorem RunsOfMultiples.sum_D_le (T : Finset ℕ) (hT : ∀ m ∈ T, 0 < m) {B : ℕ} (hB : ∀ m ∈ T, m < B) (P : Finset ℕ) (hP : P ⊆ Finset.range B) : ∑ t ∈ P, D T t ≤ ↑T.card * Real.log ↑T.card

Restricting the chain-rule sum to a sub-family of indices.