[IK]: Prove d_apply

[Ljk261]

[IK]: Prove d_apply

[zw810-ctrl]

theorem d_apply_prime_pow {k : ℕ} (hk : 0 < k) {p : ℕ} (hp : p.Prime) (a : ℕ) :
d k (p ^ a) = (a + k - 1).choose (k - 1) := by
obtain ⟨k, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (Nat.ne_of_gt hk)
induction k generalizing a with
| zero =>
rw [d_one]
simp [ArithmeticFunction.zeta_apply, hp.ne_zero]
| succ k ih =>
have hih : ∀ i : ℕ, d (k + 1) (p ^ i) = (i + k).choose k := fun i =>
ih i (Nat.succ_pos _)
rw [d_succ, mul_zeta_apply, sum_divisors_prime_pow hp]
simp_rw [hih]
simpa [Nat.add_assoc, Nat.add_left_comm, Nat.add_comm] using Nat.sum_range_add_choose a k

generated by codex.
Use mul_zeta_apply and sum_divisors_prime_pow will be easier

[AlexKontorovich]

Thanks! Proof being moved to another PR.