H3 for Thakur's hypotheses on power sums

def ZetaH123.H3.NoCarry (p j d : ℕ) (m : Fin d → ℕ) : Prop

Definition 1: the addition j + m_1 + ... + m_d (the r = d + 1 summands j, m_1, ..., m_d) has no carries in base p: at every base-p digit position t, the digits sum to at most p - 1. We read off the t-th base-p digit of a number n as (Nat.digits p n).getD t 0.

Equations

• ZetaH123.H3.NoCarry p j d m = ∀ (t : ℕ), (p.digits j).getD t 0 + ∑ i : Fin d, (p.digits (m i)).getD t 0 ≤ p - 1

def ZetaH123.H3.Tset (p q d j : ℕ) : Set (Fin d → ℕ)

Definition 2: the set T_{d,j} of d-tuples (m_1, ..., m_d) (encoded as a function Fin d → ℕ) with each m_i > 0, (q - 1) ∣ m_i, and j + m_1 + ... + m_d carry-free in base p.

Equations

• ZetaH123.H3.Tset p q d j = {m : Fin d → ℕ | (∀ (i : Fin d), 0 < m i) ∧ (∀ (i : Fin d), q - 1 ∣ m i) ∧ ZetaH123.H3.NoCarry p j d m}

def ZetaH123.H3.objective (d : ℕ) (m : Fin d → ℕ) : ℕ

The objective m_1 + 2 m_2 + ... + d m_d = ∑_{i} i · m_i (with 1-based weights; the i-th coordinate m i is weighted by i + 1 under 0-based Fin d indexing).

Equations

• ZetaH123.H3.objective d m = ∑ i : Fin d, (↑i + 1) * m i

noncomputable def ZetaH123.H3.Md (p q d j : ℕ) : ℕ

Definition 3: M_d(j) is the minimum of the objective over T_{d,j}, realized as the infimum of the image of T_{d,j} under the objective. Since T_{d,j} is nonempty (see Remarks) and ℕ is well-ordered, this minimum is attained.

Equations

• ZetaH123.H3.Md p q d j = sInf (ZetaH123.H3.objective d '' ZetaH123.H3.Tset p q d j)

noncomputable def ZetaH123.H3.sd (p q d k : ℕ) : ℕ

Definition 3: s_d(k) := d k + M_d(k - 1).

Equations

• ZetaH123.H3.sd p q d k = d * k + ZetaH123.H3.Md p q d (k - 1)

theorem ZetaH123.H3.main_theorem (p q d k f : ℕ) (hp : Nat.Prime p) (hf : 1 ≤ f) (hq : q = p ^ f) (hd : 1 ≤ d) (hk : 0 < k) (hpk : ¬p ∣ k) : sd p q d k < sd p q d (k + 1)

Theorem. Let p be a prime, q = p ^ f (f ≥ 1), and d ≥ 1, k > 0. If p ∤ k, then s_d(k) < s_d(k + 1).

theorem ZetaH123.H3.Tset_nonempty (p q d j f : ℕ) (hp : Nat.Prime p) (hf : 1 ≤ f) (hq : q = p ^ f) (hd : 1 ≤ d) : (Tset p q d j).Nonempty

Nonemptiness of T_{d,j} (Remarks): the minimization defining M_d(j) is over a nonempty set.

theorem ZetaH123.H3.Md_attained (p q d j f : ℕ) (hp : Nat.Prime p) (hf : 1 ≤ f) (hq : q = p ^ f) (hd : 1 ≤ d) : ∃ m ∈ Tset p q d j, objective d m = Md p q d j

M_d(j) is attained: there is a tuple in T_{d,j} achieving the objective value M_d(j).

theorem ZetaH123.H3.Md_le (p q d j f : ℕ) (_hp : Nat.Prime p) (_hf : 1 ≤ f) (_hq : q = p ^ f) (_hd : 1 ≤ d) {m : Fin d → ℕ} (hm : m ∈ Tset p q d j) : Md p q d j ≤ objective d m

M_d(j) is a lower bound for the objective on T_{d,j}.