the case A = perfect k-th powers

Checked by the kernel — these bytes are the ones its attestation names: attestations/000884.json, merge commit 06863fc54ca3.

import Mathlib
import Nodes.«variant-7a0f5735».Context

private def dd (n : ℕ) : ℕ := n.divisors.card

private def fk (k n : ℕ) : ℕ := (n.divisors.filter (fun e => e ^ k ∣ n)).card

private noncomputable def rk (k n : ℕ) : ℕ :=
  (Finsupp.mapRange (fun a => a / k) (Nat.zero_div k) n.factorization).prod (fun p a => p ^ a)

private lemma rk_factorization (k n : ℕ) :
    (rk k n).factorization = Finsupp.mapRange (fun a => a / k) (Nat.zero_div k) n.factorization := by
  apply Nat.prod_pow_factorization_eq_self
  intro p hp
  exact Nat.prime_of_mem_primeFactors (Finsupp.support_mapRange hp)

private lemma rk_ne_zero (k n : ℕ) : rk k n ≠ 0 := by
  unfold rk Finsupp.prod
  rw [Finset.prod_ne_zero_iff]
  intro p hp
  exact pow_ne_zero _ (Nat.prime_of_mem_primeFactors (Finsupp.support_mapRange hp)).ne_zero

private lemma pow_dvd_iff_dvd_rk {k n e : ℕ} (hk : 0 < k) (hn : n ≠ 0) (he : e ≠ 0) :
    e ^ k ∣ n ↔ e ∣ rk k n := by
  rw [← Nat.factorization_le_iff_dvd (pow_ne_zero _ he) hn,
    ← Nat.factorization_le_iff_dvd he (rk_ne_zero k n), rk_factorization, Nat.factorization_pow,
    Finsupp.le_def, Finsupp.le_def]
  apply forall_congr'; intro p
  simp only [Finsupp.smul_apply, smul_eq_mul, Finsupp.mapRange_apply]
  rw [Nat.le_div_iff_mul_le hk, mul_comm]

private lemma fk_eq_dd_rk {k n : ℕ} (hk : 0 < k) (hn : n ≠ 0) : fk k n = dd (rk k n) := by
  unfold fk dd
  congr 1
  ext e
  simp only [Finset.mem_filter, Nat.mem_divisors]
  constructor
  · rintro ⟨⟨hd, -⟩, hp⟩
    have he : e ≠ 0 := by rintro rfl; exact hn (Nat.eq_zero_of_zero_dvd hd)
    exact ⟨(pow_dvd_iff_dvd_rk hk hn he).mp hp, rk_ne_zero k n⟩
  · rintro ⟨hd, -⟩
    have he : e ≠ 0 := by rintro rfl; exact rk_ne_zero k n (Nat.eq_zero_of_zero_dvd hd)
    have hp := (pow_dvd_iff_dvd_rk hk hn he).mpr hd
    exact ⟨⟨(dvd_pow_self e hk.ne').trans hp, hn⟩, hp⟩

private lemma fk_le_dd (k n : ℕ) : fk k n ≤ dd n := Finset.card_filter_le _ _

private lemma fk_le (k n : ℕ) : fk k n ≤ n := (fk_le_dd k n).trans (Nat.card_divisors_le_self n)

private lemma fk_pos (k : ℕ) {n : ℕ} (hn : 0 < n) : 0 < fk k n := by
  unfold fk; exact Finset.card_pos.mpr ⟨1, by simp; omega⟩

private lemma pow_two_dvd_dd {n : ℕ} (hn : n ≠ 0) (S : Finset ℕ)
    (hS : ∀ p ∈ S, p.Prime ∧ p ∣ n ∧ ¬ p ^ 2 ∣ n) : 2 ^ S.card ∣ dd n := by
  unfold dd
  rw [Nat.card_divisors hn]
  have hsub : S ⊆ n.primeFactors := by
    intro p hp
    obtain ⟨h1, h2, _⟩ := hS p hp
    exact Nat.mem_primeFactors.mpr ⟨h1, h2, hn⟩
  have : 2 ^ S.card = ∏ p ∈ S, (n.factorization p + 1) := by
    rw [← Finset.prod_const]
    apply Finset.prod_congr rfl
    intro p hp
    obtain ⟨h1, h2, h3⟩ := hS p hp
    have e1 : 1 ≤ n.factorization p := (h1.dvd_iff_one_le_factorization hn).mp h2
    have e2 : ¬ 2 ≤ n.factorization p := fun h => h3 ((h1.pow_dvd_iff_le_factorization hn).mpr h)
    omega
  rw [this]
  exact Finset.prod_dvd_prod_of_subset _ _ _ hsub

private lemma pow_two_dvd_fk {k n : ℕ} (hk : 0 < k) (hn : n ≠ 0) (S : Finset ℕ)
    (hS : ∀ p ∈ S, p.Prime ∧ p ^ k ∣ n ∧ ¬ p ^ (k + 1) ∣ n) : 2 ^ S.card ∣ fk k n := by
  rw [fk_eq_dd_rk hk hn]
  apply pow_two_dvd_dd (rk_ne_zero k n)
  intro p hp
  obtain ⟨h1, h2, h3⟩ := hS p hp
  have e1 : k ≤ n.factorization p := (h1.pow_dvd_iff_le_factorization hn).mp h2
  have e2 : ¬ k + 1 ≤ n.factorization p := fun h => h3 ((h1.pow_dvd_iff_le_factorization hn).mpr h)
  have hr : (rk k n).factorization p = 1 := by
    rw [rk_factorization, Finsupp.mapRange_apply, show n.factorization p = k by omega,
      Nat.div_self hk]
  refine ⟨h1, ?_, ?_⟩
  · rw [h1.dvd_iff_one_le_factorization (rk_ne_zero k n), hr]
  · rw [h1.pow_dvd_iff_le_factorization (rk_ne_zero k n), hr]; omega


/- `1/(2^m - 1) = ∑_{j ≥ 0} (1/2)^((j+1) m)` for `m ≥ 1`. -/
private lemma one_div_two_pow_sub_one {m : ℕ} (hm : 0 < m) :
    (1 : ℝ) / (2 ^ m - 1) = ∑' j : ℕ, (1 / 2 : ℝ) ^ ((j + 1) * m) := by
  have hx0 : (0 : ℝ) ≤ (1 / 2) ^ m := by positivity
  have hx1 : (1 / 2 : ℝ) ^ m < 1 := pow_lt_one₀ (by norm_num) (by norm_num) hm.ne'
  have : ∀ j : ℕ, (1 / 2 : ℝ) ^ ((j + 1) * m) = (1 / 2) ^ m * ((1 / 2) ^ m) ^ j := by
    intro j; rw [← pow_succ', ← pow_mul, mul_comm]
  simp_rw [this]
  rw [tsum_mul_left, tsum_geometric_of_lt_one hx0 hx1]
  have h2 : (1 : ℝ) < 2 ^ m := one_lt_pow₀ (by norm_num) hm.ne'
  rw [one_div_pow]
  field_simp

/- The double-series terms. -/
private noncomputable def Gt (k : ℕ) (p : ℕ × ℕ) : ℝ := (1 / 2 : ℝ) ^ ((p.2 + 1) * (p.1 + 1) ^ k)

private lemma summable_Gt {k : ℕ} (hk : 0 < k) : Summable (Gt k) := by
  have hg : Summable (fun n : ℕ => (1 / 2 : ℝ) ^ n) := summable_geometric_two
  refine Summable.of_nonneg_of_le (fun p => by unfold Gt; positivity) (fun p => ?_)
    (hg.mul_of_nonneg hg (fun _ => by positivity) (fun _ => by positivity))
  unfold Gt
  rw [← pow_add]
  apply pow_le_pow_of_le_one (by norm_num) (by norm_num)
  have h1 : p.1 + 1 ≤ (p.1 + 1) ^ k := Nat.le_self_pow hk.ne' _
  nlinarith

/- The fibre terms. -/
private noncomputable def Ht (k : ℕ) (p : ℕ × ℕ) : ℝ :=
  if p.2 ∈ p.1.divisors.filter (fun e => e ^ k ∣ p.1) then (1 / 2 : ℝ) ^ p.1 else 0

private def phiK (k : ℕ) (p : ℕ × ℕ) : ℕ × ℕ := ((p.2 + 1) * (p.1 + 1) ^ k, p.1 + 1)

private lemma phiK_inj (k : ℕ) : Function.Injective (phiK k) := by
  rintro ⟨a, b⟩ ⟨c, d⟩ h
  simp only [phiK, Prod.mk.injEq] at h
  obtain ⟨h1, h2⟩ := h
  have hac : a = c := by omega
  subst hac
  have : b + 1 = d + 1 := Nat.eq_of_mul_eq_mul_right (by positivity) h1
  simp only [Prod.mk.injEq, true_and]; omega

private lemma Ht_phiK {k : ℕ} (hk : 0 < k) (p : ℕ × ℕ) : Ht k (phiK k p) = Gt k p := by
  unfold Ht Gt phiK
  rw [if_pos]
  simp only [Finset.mem_filter, Nat.mem_divisors]
  refine ⟨⟨?_, by positivity⟩, Dvd.intro_left _ rfl⟩
  exact (dvd_pow_self _ hk.ne').trans (Dvd.intro_left _ rfl)

private lemma support_Ht {k : ℕ} (hk : 0 < k) : Function.support (Ht k) ⊆ Set.range (phiK k) := by
  rintro ⟨N, e⟩ h
  simp only [Function.mem_support, Ht, ne_eq, ite_eq_right_iff, Classical.not_imp] at h
  obtain ⟨h, -⟩ := h
  simp only [Finset.mem_filter, Nat.mem_divisors] at h
  obtain ⟨⟨_, hN⟩, ⟨c, hc⟩⟩ := h
  have he : e ≠ 0 := by rintro rfl; simp [zero_pow hk.ne'] at hc; exact hN hc
  have hc0 : c ≠ 0 := by rintro rfl; simp at hc; exact hN hc
  refine ⟨(e - 1, c - 1), ?_⟩
  simp only [phiK, Prod.mk.injEq]
  rw [Nat.sub_add_cancel (Nat.pos_of_ne_zero he), Nat.sub_add_cancel (Nat.pos_of_ne_zero hc0), hc]
  exact ⟨mul_comm _ _, rfl⟩

private lemma tsum_Ht_fiber (k N : ℕ) : ∑' e : ℕ, Ht k (N, e) = (fk k N : ℝ) / 2 ^ N := by
  rw [tsum_eq_sum (s := N.divisors.filter (fun e => e ^ k ∣ N))]
  · unfold Ht
    simp only
    rw [Finset.sum_congr rfl (fun e he => if_pos he), Finset.sum_const, nsmul_eq_mul, fk, one_div_pow]
    ring
  · intro e he; unfold Ht; simp only; rw [if_neg he]

private lemma tsum_pow_eq {k : ℕ} (hk : 0 < k) :
    ∑' m : {m : ℕ | ∃ n, m = n ^ k}, (1 : ℝ) / (2 ^ m.1 - 1) =
      ∑' n : ℕ, (1 : ℝ) / (2 ^ (n ^ k) - 1) := by
  have hinj : Function.Injective (fun n : ℕ => n ^ k) := Nat.pow_left_injective hk.ne'
  let e : ℕ ≃ {m : ℕ | ∃ n, m = n ^ k} := Equiv.ofBijective (fun n => ⟨n ^ k, n, rfl⟩)
    ⟨fun a b h => hinj (congrArg Subtype.val h), fun ⟨m, n, hn⟩ => ⟨n, Subtype.ext hn.symm⟩⟩
  exact (e.tsum_eq (fun m => (1 : ℝ) / (2 ^ m.1 - 1))).symm

private lemma tsum_succ_eq_Gt (k n : ℕ) :
    (1 : ℝ) / (2 ^ ((n + 1) ^ k) - 1) = ∑' j : ℕ, Gt k (n, j) := by
  rw [one_div_two_pow_sub_one (by positivity)]
  rfl

/- Lambert-series identity for perfect `k`-th powers. -/
private lemma series_eq_fk {k : ℕ} (hk : 0 < k) :
    ∑' m : {m : ℕ | ∃ n, m = n ^ k}, (1 : ℝ) / (2 ^ m.1 - 1) = ∑' N : ℕ, (fk k N : ℝ) / 2 ^ N := by
  rw [tsum_pow_eq hk]
  have hs0 : Summable (fun n : ℕ => (1 : ℝ) / (2 ^ ((n + 1) ^ k) - 1)) :=
    (summable_Gt hk).prod.congr (fun n => (tsum_succ_eq_Gt k n).symm)
  rw [tsum_eq_zero_add' (f := fun n : ℕ => (1 : ℝ) / (2 ^ (n ^ k) - 1)) hs0]
  simp only [zero_pow hk.ne', pow_zero, sub_self, div_zero, zero_add]
  have h1 : ∑' n : ℕ, (1 : ℝ) / (2 ^ ((n + 1) ^ k) - 1) = ∑' p : ℕ × ℕ, Gt k p := by
    rw [(summable_Gt hk).tsum_prod]
    exact tsum_congr (tsum_succ_eq_Gt k)
  have hH : Summable (Ht k) := by
    rw [← (phiK_inj k).summable_iff (fun x hx => Function.notMem_support.mp
      (fun h => hx (support_Ht hk h)))]
    exact (summable_Gt hk).congr (fun p => (Ht_phiK hk p).symm)
  have h2 : ∑' p : ℕ × ℕ, Gt k p = ∑' p : ℕ × ℕ, Ht k p := by
    rw [← (phiK_inj k).tsum_eq (support_Ht hk)]
    exact tsum_congr (fun p => (Ht_phiK hk p).symm)
  rw [h1, h2, hH.tsum_prod]
  exact tsum_congr (fun N => tsum_Ht_fiber k N)


/- `b` times the "tail" `∑_{i ≥ 1} f_k(j+i) / 2^i`. -/
private noncomputable def Tail (k b : ℕ) (j : ℕ) : ℝ := b * ∑' i : ℕ, (fk k (j + i + 1) : ℝ) / 2 ^ (i + 1)

/- The integer that the tail equals when the series is `a / b`. -/
private def Zint (k : ℕ) (a : ℤ) (b : ℕ) (j : ℕ) : ℤ :=
  a * 2 ^ j - b * ∑ n ∈ Finset.range (j + 1), (fk k n : ℤ) * 2 ^ (j - n)


private lemma summable_fk_shift (k : ℕ) (j : ℕ) : Summable (fun i : ℕ => (fk k (j + i + 1) : ℝ) / 2 ^ (i + 1)) := by
  have h : Summable (fun i : ℕ => ((j + 1 : ℝ) + i) * (1/2) ^ i) := by
    have h1 := (summable_geometric_two).mul_left (j+1 : ℝ)
    have h2 := summable_pow_mul_geometric_of_norm_lt_one 1 (r := (1/2 : ℝ))
      (by norm_num [abs_of_pos])
    simpa [add_mul] using h1.add h2
  refine Summable.of_nonneg_of_le (fun i => by positivity) (fun i => ?_) h
  have : (fk k (j + i + 1) : ℝ) ≤ j + i + 1 := by exact_mod_cast fk_le k _
  rw [div_eq_mul_inv, pow_succ, mul_inv, one_div, inv_pow]
  have : (0:ℝ) ≤ (2 ^ i)⁻¹ := by positivity
  nlinarith

private lemma summable_fk (k : ℕ) : Summable (fun n : ℕ => (fk k n : ℝ) / 2 ^ n) := by
  have h2 := summable_pow_mul_geometric_of_norm_lt_one 1 (r := (1/2 : ℝ))
    (by norm_num [abs_of_pos])
  refine Summable.of_nonneg_of_le (fun i => by positivity) (fun i => ?_) h2
  have : (fk k i : ℝ) ≤ i := by exact_mod_cast fk_le k _
  rw [div_eq_mul_inv, one_div, inv_pow, pow_one]
  have : (0:ℝ) ≤ (2 ^ i)⁻¹ := by positivity
  nlinarith

private lemma tail_pos (k : ℕ) {b : ℕ} (hb : 0 < b) (j : ℕ) : 0 < Tail k b j := by
  unfold Tail
  apply mul_pos (by exact_mod_cast hb)
  apply (summable_fk_shift k j).tsum_pos (fun i => by positivity) 0
  have := fk_pos k (n := j + 0 + 1) (by omega)
  positivity

private lemma tail_upper (k : ℕ) (b j L : ℕ) :
    Tail k b j ≤ b * ∑ i ∈ Finset.range L, (fk k (j + i + 1) : ℝ) / 2 ^ (i + 1)
      + b * ((j + L + 2 : ℝ) / 2 ^ L) := by
  unfold Tail
  rw [← (summable_fk_shift k j).sum_add_tsum_nat_add L, mul_add]
  gcongr
  have hg1 : Summable (fun i : ℕ => (1/2 : ℝ) ^ i) := summable_geometric_two
  have hg2 : Summable (fun i : ℕ => (i : ℝ) * (1/2 : ℝ) ^ i) := by
    simpa using summable_pow_mul_geometric_of_norm_lt_one 1 (r := (1/2 : ℝ))
      (by norm_num [abs_of_pos])
  have key : ∑' i : ℕ, ((j + L + 1 : ℝ) / 2 ^ (L + 1) * (1/2) ^ i
      + 1 / 2 ^ (L + 1) * ((i : ℝ) * (1/2) ^ i)) = (j + L + 2 : ℝ) / 2 ^ L := by
    rw [(hg1.mul_left _).tsum_add (hg2.mul_left _), tsum_mul_left, tsum_mul_left,
      tsum_geometric_two, tsum_coe_mul_geometric_of_norm_lt_one (by norm_num [abs_of_pos])]
    rw [pow_succ]; field_simp; ring
  rw [← key]
  refine Summable.tsum_le_tsum (fun i => ?_) ((summable_nat_add_iff L).mpr (summable_fk_shift k j))
    ((hg1.mul_left _).add (hg2.mul_left _))
  have : (fk k (j + (i + L) + 1) : ℝ) ≤ j + L + 1 + i := by
    have := fk_le k (j + (i + L) + 1)
    have : (fk k (j + (i + L) + 1) : ℝ) ≤ ((j + (i + L) + 1 : ℕ) : ℝ) := by exact_mod_cast this
    push_cast at this; linarith
  show (fk k (j + (i + L) + 1) : ℝ) / 2 ^ (i + L + 1) ≤ _
  rw [show (2:ℝ) ^ (i + L + 1) = 2 ^ (L+1) * 2 ^ i by ring, one_div_pow]
  rw [div_le_iff₀ (by positivity)]
  field_simp
  linarith

private lemma tail_eq_Zint (k : ℕ) {a : ℤ} {b : ℕ} (hb : 0 < b)
    (h : ∑' n : ℕ, (fk k n : ℝ) / 2 ^ n = a / b) (j : ℕ) : Tail k b j = Zint k a b j := by
  have hsplit := (summable_fk k).sum_add_tsum_nat_add (j + 1)
  have htail : ∑' i : ℕ, (fk k (i + (j + 1)) : ℝ) / 2 ^ (i + (j + 1)) =
      (1 / 2 ^ j) * ∑' i : ℕ, (fk k (j + i + 1) : ℝ) / 2 ^ (i + 1) := by
    rw [← tsum_mul_left]
    apply tsum_congr; intro i
    rw [show i + (j + 1) = j + i + 1 by ring,
      show (2:ℝ) ^ (j + i + 1) = 2 ^ j * 2 ^ (i + 1) by ring]
    field_simp
  rw [htail, h] at hsplit
  have hb' : (b : ℝ) ≠ 0 := by exact_mod_cast hb.ne'
  have hT : Tail k b j = 2 ^ j * (a - b * ∑ n ∈ Finset.range (j + 1), (fk k n : ℝ) / 2 ^ n) := by
    unfold Tail
    field_simp at hsplit
    have : (2:ℝ) ^ j ≠ 0 := by positivity
    field_simp
    linear_combination hsplit
  rw [hT]
  unfold Zint
  push_cast
  rw [mul_sub, Finset.mul_sum, Finset.mul_sum, Finset.mul_sum]
  congr 1
  · ring
  · apply Finset.sum_congr rfl; intro n hn
    have hn' : n ≤ j := Nat.lt_succ_iff.mp (Finset.mem_range.mp hn)
    rw [pow_sub₀ _ (by norm_num) hn']
    field_simp

private lemma Zint_dvd (k : ℕ) (a : ℤ) (b s m : ℕ) (hd : ∀ n, s < n → n ≤ s + m → 2 ^ m ∣ fk k n) :
    (2 : ℤ) ^ m ∣ Zint k a b (s + m) := by
  unfold Zint
  apply dvd_sub
  · exact Dvd.dvd.mul_left (pow_dvd_pow 2 (by omega)) _
  · apply Dvd.dvd.mul_left
    apply Finset.dvd_sum
    intro n hn
    have hn' : n ≤ s + m := Nat.lt_succ_iff.mp (Finset.mem_range.mp hn)
    by_cases hnk : n ≤ s
    · exact Dvd.dvd.mul_left (pow_dvd_pow 2 (by omega)) _
    · apply Dvd.dvd.mul_right
      exact_mod_cast hd n (by omega) hn'


private lemma dd_le_two_mul_small (n : ℕ) :
    dd n ≤ 2 * (n.divisors.filter (fun e => e * e ≤ n)).card := by
  unfold dd
  rw [← Finset.card_filter_add_card_filter_not (fun e => e * e ≤ n)]
  have : (n.divisors.filter (fun e => ¬ e * e ≤ n)).card ≤
      (n.divisors.filter (fun e => e * e ≤ n)).card := by
    apply Finset.card_le_card_of_injOn (fun e => n / e)
    · intro e he
      simp only [Finset.coe_filter, Nat.mem_divisors, not_le, Set.mem_setOf_eq] at he ⊢
      obtain ⟨⟨hd, hn⟩, hlt⟩ := he
      have hepos : 0 < e := Nat.pos_of_dvd_of_pos hd (Nat.pos_of_ne_zero hn)
      refine ⟨⟨Nat.div_dvd_of_dvd hd, hn⟩, ?_⟩
      have h1 : n / e < e := (Nat.div_lt_iff_lt_mul hepos).mpr hlt
      calc n / e * (n / e) ≤ n / e * e := Nat.mul_le_mul_left _ h1.le
        _ = n := Nat.div_mul_cancel hd
    · intro e1 h1 e2 h2 h
      simp only [Finset.coe_filter, Nat.mem_divisors, Set.mem_setOf_eq] at h1 h2
      have := congrArg (fun x => n / x) h
      simp only at this
      rwa [Nat.div_div_self h1.1.1 h1.1.2, Nat.div_div_self h2.1.1 h2.1.2] at this
  omega

private lemma card_AP_dvd_le (r Q X e : ℕ) (hcop : Nat.Coprime r Q) :
    ((Finset.range X).filter (fun t => (e + 1) ∣ r + t * Q)).card ≤ X / (e + 1) + 1 := by
  set E := e + 1 with hE
  have hEpos : 0 < E := by omega
  have key : ∀ t1 ∈ (Finset.range X).filter (fun t => E ∣ r + t * Q),
      ∀ t2 ∈ (Finset.range X).filter (fun t => E ∣ r + t * Q), t1 / E = t2 / E → t1 ≤ t2 → t1 = t2 := by
    intro t1 h1 t2 h2 hq hle
    simp only [Finset.mem_filter, Finset.mem_range] at h1 h2
    have hcopE : Nat.Coprime E Q := by
      have hg1 : Nat.gcd E Q ∣ r + t1 * Q := (Nat.gcd_dvd_left E Q).trans h1.2
      have hg2 : Nat.gcd E Q ∣ t1 * Q := Dvd.dvd.mul_left (Nat.gcd_dvd_right E Q) _
      have hg3 : Nat.gcd E Q ∣ r := (Nat.dvd_add_left hg2).mp hg1
      have hg4 : Nat.gcd E Q ∣ Nat.gcd r Q := Nat.dvd_gcd hg3 (Nat.gcd_dvd_right E Q)
      rw [hcop] at hg4
      exact Nat.dvd_one.mp hg4
    have hd : E ∣ (t2 - t1) * Q := by
      have := Nat.dvd_sub h2.2 h1.2
      rwa [show r + t2 * Q - (r + t1 * Q) = (t2 - t1) * Q by rw [Nat.sub_mul]; omega] at this
    have hd2 : E ∣ t2 - t1 := hcopE.dvd_of_dvd_mul_right hd
    have hlt : t2 - t1 < E := by
      have e1 := Nat.div_add_mod t1 E
      have e2 := Nat.div_add_mod t2 E
      have m1 := Nat.mod_lt t1 hEpos
      have m2 := Nat.mod_lt t2 hEpos
      rw [hq] at e1
      omega
    have := Nat.eq_zero_of_dvd_of_lt hd2 hlt
    omega
  calc ((Finset.range X).filter (fun t => E ∣ r + t * Q)).card ≤ (Finset.range (X / E + 1)).card := by
        apply Finset.card_le_card_of_injOn (fun t => t / E)
        · intro t ht
          simp only [Finset.coe_filter, Finset.mem_range, Set.mem_setOf_eq] at ht
          simp only [Finset.coe_range, Set.mem_Iio]
          have := Nat.div_le_div_right (c := E) ht.1.le
          omega
        · intro t1 h1 t2 h2 hq
          rcases le_total t1 t2 with h | h
          · exact key t1 h1 t2 h2 hq h
          · exact (key t2 h2 t1 h1 hq.symm h).symm
    _ = X / E + 1 := Finset.card_range _

private lemma sum_dd_AP_le (r Q X : ℕ) (hcop : Nat.Coprime r Q)
    (hX : ∀ t < X, r + t * Q ≤ X * X) :
    (∑ t ∈ Finset.range X, (dd (r + t * Q) : ℝ)) ≤ 2 * X * (2 + Real.log X) := by
  have hnat : ∑ t ∈ Finset.range X, dd (r + t * Q) ≤ 2 * ∑ e ∈ Finset.range X, (X / (e + 1) + 1) := by
    calc ∑ t ∈ Finset.range X, dd (r + t * Q)
        ≤ ∑ t ∈ Finset.range X, 2 * ((Finset.range X).filter (fun e => (e + 1) ∣ r + t * Q)).card := by
          apply Finset.sum_le_sum; intro t ht
          refine (dd_le_two_mul_small _).trans ?_
          apply Nat.mul_le_mul_left
          apply Finset.card_le_card_of_injOn (fun e => e - 1)
          · intro e he
            simp only [Finset.coe_filter, Nat.mem_divisors, Set.mem_setOf_eq] at he
            simp only [Finset.coe_filter, Finset.mem_range, Set.mem_setOf_eq]
            have hepos : 0 < e := Nat.pos_of_dvd_of_pos he.1.1 (Nat.pos_of_ne_zero he.1.2)
            have : e * e ≤ X * X := he.2.trans (hX t (by simpa using ht))
            have : e ≤ X := Nat.mul_self_le_mul_self_iff.mp this
            refine ⟨by omega, ?_⟩
            rw [Nat.sub_add_cancel hepos]; exact he.1.1
          · intro e1 h1 e2 h2 h
            simp only [Finset.coe_filter, Nat.mem_divisors, Set.mem_setOf_eq] at h1 h2
            have := Nat.pos_of_dvd_of_pos h1.1.1 (Nat.pos_of_ne_zero h1.1.2)
            have := Nat.pos_of_dvd_of_pos h2.1.1 (Nat.pos_of_ne_zero h2.1.2)
            simp only at h
            omega
      _ = 2 * ∑ e ∈ Finset.range X, ((Finset.range X).filter (fun t => (e + 1) ∣ r + t * Q)).card := by
          rw [← Finset.mul_sum]
          congr 1
          simp only [Finset.card_filter]
          exact Finset.sum_comm
      _ ≤ 2 * ∑ e ∈ Finset.range X, (X / (e + 1) + 1) := by
          apply Nat.mul_le_mul_left
          exact Finset.sum_le_sum fun e _ => card_AP_dvd_le r Q X e hcop
  have hreal : ((∑ e ∈ Finset.range X, (X / (e + 1) + 1) : ℕ) : ℝ) ≤ X * (1 + Real.log X) + X := by
    push_cast
    rw [Finset.sum_add_distrib]
    simp only [Finset.sum_const, Finset.card_range, nsmul_eq_mul, mul_one]
    gcongr
    calc ∑ e ∈ Finset.range X, ((X / (e + 1) : ℕ) : ℝ) ≤ ∑ e ∈ Finset.range X, (X : ℝ) / (e + 1) := by
          apply Finset.sum_le_sum; intro e _
          have := Nat.cast_div_le (α := ℝ) (m := X) (n := e + 1)
          push_cast at this; exact this
      _ = X * (harmonic X : ℝ) := by
          rw [harmonic]; push_cast; rw [Finset.mul_sum]
          apply Finset.sum_congr rfl; intro e _; field_simp
      _ ≤ X * (1 + Real.log X) := by
          gcongr
          exact harmonic_le_one_add_log X
  have h1 : (∑ t ∈ Finset.range X, (dd (r + t * Q) : ℝ)) ≤
      2 * ((∑ e ∈ Finset.range X, (X / (e + 1) + 1) : ℕ) : ℝ) := by
    exact_mod_cast hnat
  linarith

private lemma idx_inj {m i j i' j' : ℕ} (hj : j < m) (hj' : j' < m) (h : i * m + j = i' * m + j') :
    i = i' ∧ j = j' := by
  rcases lt_trichotomy i i' with hi | hi | hi
  · exfalso
    have : (i + 1) * m ≤ i' * m := Nat.mul_le_mul_right _ hi
    nlinarith
  · subst hi; omega
  · exfalso
    have : (i' + 1) * m ≤ i * m := Nat.mul_le_mul_right _ hi
    nlinarith

private lemma sum_fk_AP_le (k r Q X : ℕ) (hcop : Nat.Coprime r Q)
    (hX : ∀ t < X, r + t * Q ≤ X * X) :
    (∑ t ∈ Finset.range X, (fk k (r + t * Q) : ℝ)) ≤ 2 * X * (2 + Real.log X) := by
  refine le_trans ?_ (sum_dd_AP_le r Q X hcop hX)
  exact Finset.sum_le_sum fun t _ => by exact_mod_cast fk_le_dd k _

/- The averaging contradiction: the lower bounds `2^m ≤ Tail` along an arithmetic progression
are incompatible with the average size of the divisor function. -/
private lemma averaging_contra {k b m q Q c : ℕ} (hb : 0 < b) (hQpos : 0 < Q) (hcQ : c < Q)
    (hQle : Q ≤ 2 ^ q) (hA2 : m + 3 * q ≤ 2 ^ q) (hA3 : 8 * b ≤ 2 ^ q)
    (hA4 : 2 * b * (3 + q) + 1 < 2 ^ m)
    (hcop : ∀ i < 3 * q, Nat.Coprime (c + m + i + 1) Q)
    (hlow : ∀ t, (2 : ℝ) ^ m ≤ Tail k b (c + t * Q + m)) : False := by
  set L := 3 * q with hLdef
  set X := Q + m + L with hXdef
  -- numerical facts
  have hX1 : 1 ≤ X := by omega
  have hXpow : X ≤ 2 ^ (q + 1) := by rw [pow_succ]; omega
  have hLX : 2 * b * X ^ 2 ≤ 2 ^ L := by
    calc 2 * b * X ^ 2 ≤ 2 * b * (2 ^ (q + 1)) ^ 2 := by gcongr
      _ = 8 * b * (2 ^ q * 2 ^ q) := by ring
      _ ≤ 2 ^ q * (2 ^ q * 2 ^ q) := by gcongr
      _ = 2 ^ L := by rw [hLdef]; ring
  have hrange : ∀ t < X, c + t * Q < X * Q := by
    intro t ht
    have : (t + 1) * Q ≤ X * Q := Nat.mul_le_mul_right _ ht
    nlinarith
  have hXX : X * Q + m + L ≤ X * X := by
    have : X * X = X * Q + X * (m + L) := by rw [hXdef]; ring
    have : m + L ≤ X * (m + L) := Nat.le_mul_of_pos_left _ hX1
    omega
  -- upper bound for each t
  have hupt : ∀ t < X, Tail k b (c + t * Q + m) ≤
      b * ∑ i ∈ Finset.range L, (fk k (c + m + i + 1 + t * Q) : ℝ) / 2 ^ (i + 1)
        + b * ((2 * X ^ 2 : ℕ) / 2 ^ L : ℝ) := by
    intro t ht
    have h := tail_upper k b (c + t * Q + m) L
    have e : ∀ i, c + t * Q + m + i + 1 = c + m + i + 1 + t * Q := fun i => by ring
    simp only [e] at h
    refine h.trans (add_le_add le_rfl ?_)
    gcongr
    have := hrange t ht
    have h2 : c + t * Q + m + L + 2 ≤ 2 * X ^ 2 := by nlinarith
    exact_mod_cast h2
  have hgeom : ∀ L : ℕ, ∑ i ∈ Finset.range L, (1 / 2 : ℝ) ^ (i + 1) ≤ 1 := by
    intro L
    have : ∑ i ∈ Finset.range L, (1 / 2 : ℝ) ^ (i + 1) = 1 - (1 / 2) ^ L := by
      induction L with
      | zero => simp
      | succ n ih => rw [Finset.sum_range_succ, ih]; ring
    rw [this]; linarith [pow_pos (by norm_num : (0 : ℝ) < 1 / 2) L]
  set B : ℝ := 2 * X * (2 + Real.log X) with hBdef
  have hF : ∀ i ∈ Finset.range L, (∑ t ∈ Finset.range X, (fk k (c + m + i + 1 + t * Q) : ℝ)) ≤ B := by
    intro i hi
    apply sum_fk_AP_le _ _ _ _ (hcop i (by simpa using hi))
    intro t ht
    have := hrange t ht
    have : i < L := by simpa using hi
    omega
  have hB0 : 0 ≤ B := by
    have : 0 ≤ Real.log X := Real.log_nonneg (by exact_mod_cast hX1)
    positivity
  have hmain : (X : ℝ) * 2 ^ m ≤ b * B + X := by
    calc (X : ℝ) * 2 ^ m = ∑ t ∈ Finset.range X, (2 : ℝ) ^ m := by simp
      _ ≤ ∑ t ∈ Finset.range X, Tail k b (c + t * Q + m) := Finset.sum_le_sum fun t _ => hlow t
      _ ≤ ∑ t ∈ Finset.range X, (b * ∑ i ∈ Finset.range L, (fk k (c + m + i + 1 + t * Q) : ℝ) / 2 ^ (i + 1)
            + b * ((2 * X ^ 2 : ℕ) / 2 ^ L : ℝ)) :=
          Finset.sum_le_sum fun t ht => hupt t (by simpa using ht)
      _ = b * ∑ i ∈ Finset.range L, (∑ t ∈ Finset.range X, (fk k (c + m + i + 1 + t * Q) : ℝ)) * (1 / 2) ^ (i + 1)
            + X * (b * ((2 * X ^ 2 : ℕ) / 2 ^ L : ℝ)) := by
          rw [Finset.sum_add_distrib, ← Finset.mul_sum, Finset.sum_comm]
          simp only [Finset.sum_const, Finset.card_range, nsmul_eq_mul, Finset.sum_mul, div_eq_mul_inv,
            inv_pow, one_mul]
      _ ≤ b * ∑ i ∈ Finset.range L, B * (1 / 2) ^ (i + 1) + X * 1 := by
          apply add_le_add
          · apply mul_le_mul_of_nonneg_left _ (Nat.cast_nonneg _)
            apply Finset.sum_le_sum
            intro i hi
            exact mul_le_mul_of_nonneg_right (hF i hi) (by positivity)
          · apply mul_le_mul_of_nonneg_left _ (Nat.cast_nonneg _)
            rw [← mul_div_assoc, div_le_one (by positivity)]
            have h1 : b * (2 * X ^ 2) ≤ 2 ^ L := by
              calc b * (2 * X ^ 2) = 2 * b * X ^ 2 := by ring
                _ ≤ 2 ^ L := hLX
            exact_mod_cast h1
      _ ≤ b * B + X := by
          rw [← Finset.mul_sum, mul_one]
          apply add_le_add_left
          apply mul_le_mul_of_nonneg_left _ (Nat.cast_nonneg _)
          calc B * ∑ i ∈ Finset.range L, (1 / 2 : ℝ) ^ (i + 1) ≤ B * 1 :=
                mul_le_mul_of_nonneg_left (hgeom L) hB0
            _ = B := mul_one B
  have hXpos : (0 : ℝ) < X := by exact_mod_cast hX1
  have h2m : (2 : ℝ) ^ m ≤ 2 * b * (2 + Real.log X) + 1 := by
    have : (X : ℝ) * 2 ^ m ≤ X * (2 * b * (2 + Real.log X) + 1) := by
      rw [hBdef] at hmain; nlinarith
    exact le_of_mul_le_mul_left this hXpos
  have hlogX : Real.log X ≤ q + 1 := by
    calc Real.log X ≤ Real.log ((2 : ℝ) ^ (q + 1)) :=
          Real.log_le_log hXpos (by exact_mod_cast hXpow)
      _ = (q + 1) * Real.log 2 := by rw [Real.log_pow]; push_cast; ring
      _ ≤ (q + 1) * 1 := by
          gcongr
          linarith [Real.log_two_lt_d9]
      _ = q + 1 := mul_one _
  have hA4' : (2 * b * (3 + q) + 1 : ℝ) < 2 ^ m := by exact_mod_cast hA4
  have : (2 * b * (2 + Real.log X) + 1 : ℝ) ≤ 2 * b * (3 + q) + 1 := by
    have : (0 : ℝ) ≤ b := by positivity
    nlinarith
  linarith


private lemma exists_param (b k : ℕ) : ∃ m : ℕ, b ≤ m ∧ k ≤ m ∧ 1 ≤ m ∧ 15 * m ^ 6 < 2 ^ m := by
  have h := tendsto_pow_const_div_const_pow_of_one_lt 6 (r := (2:ℝ)) (by norm_num)
  have h2 := (h.eventually (gt_mem_nhds (show (0:ℝ) < 1/15 by norm_num))).and
    (Filter.eventually_ge_atTop (max (max b k) 1))
  obtain ⟨m, hm, hmb⟩ := h2.exists
  refine ⟨m, le_of_max_le_left (le_of_max_le_left hmb), le_of_max_le_right (le_of_max_le_left hmb),
    le_of_max_le_right hmb, ?_⟩
  have : (m : ℝ) ^ 6 < 1 / 15 * 2 ^ m := by
    rwa [div_lt_iff₀ (by positivity)] at hm
  have : (15 * m ^ 6 : ℝ) < 2 ^ m := by linarith
  exact_mod_cast this

/- Numerical facts about the parameters. -/
private lemma param_facts {b k m : ℕ} (hbm : b ≤ m) (hkm : k ≤ m) (hm1 : 1 ≤ m)
    (hm : 15 * m ^ 6 < 2 ^ m) :
    let q := (k + 1) * (m + m * m) * (m * m)
    m + 3 * q < 2 ^ m ∧ m + 3 * q ≤ 2 ^ q ∧ 8 * b ≤ 2 ^ q ∧ 2 * b * (3 + q) + 1 < 2 ^ m := by
  intro q
  have hq5 : q ≤ 4 * m ^ 5 := by
    have : m + m * m ≤ 2 * (m * m) := by nlinarith
    calc q ≤ (2 * m) * (2 * (m * m)) * (m * m) := by simp only [q]; gcongr; omega
      _ = 4 * m ^ 5 := by ring
  have hm56 : m ^ 5 ≤ m ^ 6 := Nat.pow_le_pow_right hm1 (by norm_num)
  have hm6 : m ≤ m ^ 6 := by
    calc m = m ^ 1 := (pow_one m).symm
      _ ≤ m ^ 6 := Nat.pow_le_pow_right hm1 (by norm_num)
  have hmq : m ≤ q := by
    simp only [q]
    have : 1 ≤ (k + 1) * (m + m * m) := by nlinarith
    nlinarith
  have h2q : 2 ^ m ≤ 2 ^ q := Nat.pow_le_pow_right (by norm_num) hmq
  refine ⟨by omega, by omega, by omega, ?_⟩
  have : b * (3 + q) ≤ m * (3 + 4 * m ^ 5) := Nat.mul_le_mul hbm (by omega)
  have : m * (3 + 4 * m ^ 5) = 3 * m + 4 * m ^ 6 := by ring
  have : 2 * b * (3 + q) = 2 * (b * (3 + q)) := by ring
  omega

private theorem irrational_fk_series {k : ℕ} (hk0 : 0 < k) :
    Irrational (∑' n : ℕ, (fk k n : ℝ) / 2 ^ n) := by
  rintro ⟨qr, hq⟩
  set a : ℤ := qr.num
  set b : ℕ := qr.den
  have hb : 0 < b := qr.pos
  have hx : ∑' n : ℕ, (fk k n : ℝ) / 2 ^ n = a / b := by
    rw [← hq]; exact Rat.cast_def qr
  have hT : ∀ j, Tail k b j = Zint k a b j := tail_eq_Zint k hb hx
  obtain ⟨m, hbm, hkm, hm1, hm⟩ := exists_param b k
  obtain ⟨hA1, hA2, hA3, hA4⟩ := param_facts hbm hkm hm1 hm
  set q := (k + 1) * (m + m * m) * (m * m) with hqdef
  have hbert : ∀ e : ℕ, ∃ p, p.Prime ∧ 2 ^ e < p ∧ p ≤ 2 * 2 ^ e :=
    fun e => Nat.exists_prime_lt_and_le_two_mul _ (by positivity)
  choose P hPp hPlo hPhi using hbert
  have hPmono : ∀ e e', e < e' → P e < P e' := by
    intro e e' h
    calc P e ≤ 2 * 2 ^ e := hPhi e
      _ = 2 ^ (e + 1) := by ring
      _ ≤ 2 ^ e' := Nat.pow_le_pow_right (by norm_num) h
      _ < P e' := hPlo e'
  have hPinj : ∀ e e', P e = P e' → e = e' := by
    intro e e' h
    rcases lt_trichotomy e e' with h' | h' | h'
    · exact absurd h (hPmono _ _ h').ne
    · exact h'
    · exact absurd h (hPmono _ _ h').ne'
  set pr : ℕ × ℕ → ℕ := fun ij => P (m + ij.1 * m + ij.2) with hprdef
  set S : Finset (ℕ × ℕ) := Finset.range m ×ˢ Finset.range m with hSdef
  have hprp : ∀ ij, (pr ij).Prime := fun ij => hPp _
  have hprlo : ∀ ij, 2 ^ m < pr ij := by
    intro ij
    calc 2 ^ m ≤ 2 ^ (m + ij.1 * m + ij.2) := Nat.pow_le_pow_right (by norm_num) (by omega)
      _ < pr ij := hPlo _
  have hprhi : ∀ ij ∈ S, pr ij ≤ 2 ^ (m + m * m) := by
    intro ij hij
    simp only [hSdef, Finset.mem_product, Finset.mem_range] at hij
    have : ij.1 * m + ij.2 + 1 ≤ m * m := by
      have : (ij.1 + 1) * m ≤ m * m := Nat.mul_le_mul_right _ (by omega)
      nlinarith
    calc pr ij ≤ 2 * 2 ^ (m + ij.1 * m + ij.2) := hPhi _
      _ = 2 ^ (m + ij.1 * m + ij.2 + 1) := by ring
      _ ≤ 2 ^ (m + m * m) := Nat.pow_le_pow_right (by norm_num) (by omega)
  have hinj : Set.InjOn pr (S : Set (ℕ × ℕ)) := by
    intro x hx y hy hxy
    simp only [hSdef, Finset.coe_product, Finset.coe_range, Set.mem_prod, Set.mem_Iio] at hx hy
    have h1 := hPinj _ _ hxy
    have h2 : x.1 * m + x.2 = y.1 * m + y.2 := by omega
    obtain ⟨e1, e2⟩ := idx_inj hx.2 hy.2 h2
    exact Prod.ext e1 e2
  set Q : ℕ := ∏ ij ∈ S, pr ij ^ (k + 1) with hQdef
  have hQpos : 0 < Q := Finset.prod_pos (fun ij _ => pow_pos (hprp ij).pos (k + 1))
  have hQle : Q ≤ 2 ^ q := by
    calc Q ≤ ((2 ^ (m + m * m)) ^ (k + 1)) ^ S.card := by
          apply Finset.prod_le_pow_card
          intro ij hij
          exact Nat.pow_le_pow_left (hprhi ij hij) (k + 1)
      _ = 2 ^ q := by
          rw [hSdef, Finset.card_product, Finset.card_range, ← pow_mul, ← pow_mul, hqdef]
          ring_nf
  set L := 3 * q with hLdef
  have hdvdQ : ∀ ij ∈ S, pr ij ^ (k + 1) ∣ Q := fun ij hij => Finset.dvd_prod_of_mem _ hij
  -- Chinese remainder theorem
  have hs : ∀ ij ∈ S, pr ij ^ (k + 1) ≠ 0 := fun ij _ => (pow_pos (hprp ij).pos (k + 1)).ne'
  have pp : Set.Pairwise (S : Set (ℕ × ℕ))
      (Function.onFun Nat.Coprime fun ij => pr ij ^ (k + 1)) := by
    intro x hx y hy hxy
    exact Nat.Coprime.pow (k + 1) (k + 1) ((Nat.coprime_primes (hprp x) (hprp y)).2
      (fun h => hxy (hinj hx hy h)))
  set crt := Nat.chineseRemainderOfFinset (fun ij => pr ij ^ (k + 1) + pr ij ^ k - (ij.1 + 1))
    (fun ij => pr ij ^ (k + 1)) S hs pp
  set c : ℕ := crt.1
  have hc : ∀ ij ∈ S, c ≡ pr ij ^ (k + 1) + pr ij ^ k - (ij.1 + 1) [MOD pr ij ^ (k + 1)] := crt.2
  have hcQ : c < Q := Nat.chineseRemainderOfFinset_lt_prod _ _ hs pp
  -- the key congruence
  have hcong : ∀ t, ∀ ij ∈ S, c + t * Q + (ij.1 + 1) ≡ pr ij ^ k [MOD pr ij ^ (k + 1)] := by
    intro t ij hij
    obtain ⟨R, hR⟩ := hdvdQ ij hij
    have hi : ij.1 < m := by
      simp only [hSdef, Finset.mem_product, Finset.mem_range] at hij; exact hij.1
    have hp := hprlo ij
    have hm2 : m < 2 ^ m := Nat.lt_two_pow_self
    have hpk : pr ij ≤ pr ij ^ k := Nat.le_self_pow hk0.ne' _
    have e1 : c + t * Q ≡ c [MOD pr ij ^ (k + 1)] := by
      rw [hR, show t * (pr ij ^ (k + 1) * R) = pr ij ^ (k + 1) * (t * R) by ring]
      exact Nat.add_mul_mod_self_left _ _ _
    have e2 := (e1.trans (hc ij hij)).add_right (ij.1 + 1)
    rw [Nat.sub_add_cancel (by omega)] at e2
    refine e2.trans ?_
    exact Nat.add_mod_left _ _
  -- forced divisibility
  have hforced : ∀ t, ∀ n, c + t * Q < n → n ≤ c + t * Q + m → 2 ^ m ∣ fk k n := by
    intro t n hn1 hn2
    obtain ⟨i, rfl⟩ : ∃ i, n = c + t * Q + (i + 1) := ⟨n - (c + t * Q) - 1, by omega⟩
    have hi : i < m := by omega
    have hcard : ((Finset.range m).image (fun j => pr (i, j))).card = m := by
      rw [Finset.card_image_of_injOn, Finset.card_range]
      intro j hj j' hj' h
      have := hinj (by simp [hSdef, hi, (by simpa using hj : j < m)])
        (by simp [hSdef, hi, (by simpa using hj' : j' < m)]) h
      simpa using this
    rw [← hcard]
    apply pow_two_dvd_fk hk0 (by omega)
    intro p hp
    obtain ⟨j, hj, rfl⟩ := Finset.mem_image.mp hp
    have hij : (i, j) ∈ S := by simp [hSdef, hi, (by simpa using hj : j < m)]
    have h := hcong t (i, j) hij
    have hpp := hprp (i, j)
    refine ⟨hpp, (h.dvd_iff (pow_dvd_pow _ (Nat.le_succ k))).2 dvd_rfl, ?_⟩
    rw [h.dvd_iff dvd_rfl]
    intro hd
    have := (Nat.pow_dvd_pow_iff_le_right hpp.one_lt).mp hd
    omega
  -- coprimality
  have hcop : ∀ i < L, Nat.Coprime (c + m + i + 1) Q := by
    intro i hi
    apply Nat.Coprime.prod_right
    intro ij hij
    apply Nat.Coprime.pow_right
    rw [Nat.coprime_comm, Nat.Prime.coprime_iff_not_dvd (hprp ij)]
    intro hd
    have hi0 : ij.1 < m := by
      simp only [hSdef, Finset.mem_product, Finset.mem_range] at hij; exact hij.1
    have h1 : pr ij ∣ c + 0 * Q + (ij.1 + 1) :=
      ((hcong 0 ij hij).dvd_iff ((dvd_pow_self _ hk0.ne').trans (pow_dvd_pow _ (Nat.le_succ k)))).2
        (dvd_pow_self _ hk0.ne')
    have h2 : c + m + i + 1 = (c + 0 * Q + (ij.1 + 1)) + (m + i - ij.1) := by omega
    rw [h2] at hd
    have h3 := (Nat.dvd_add_right h1).mp hd
    have h4 := Nat.le_of_dvd (by omega) h3
    have := hprlo ij
    have hm2 : m < 2 ^ m := Nat.lt_two_pow_self
    omega
  -- lower bound
  have hlow : ∀ t, (2 : ℝ) ^ m ≤ Tail k b (c + t * Q + m) := by
    intro t
    have hd := Zint_dvd k a b (c + t * Q) m (hforced t)
    have hpos := tail_pos k hb (c + t * Q + m)
    rw [hT] at hpos ⊢
    have hpos' : 0 < Zint k a b (c + t * Q + m) := by exact_mod_cast hpos
    have := Int.le_of_dvd hpos' hd
    exact_mod_cast this
  exact averaging_contra hb hQpos hcQ hQle hA2 hA3 hA4 hcop hlow

/-- Erdős 257 for `A` the perfect `k`-th powers `{n^k}`, for every `k ≥ 1`. Known: D. Duverney
and Y. Tachiya, *Refinement of the Chowla–Erdős method and linear independence of certain
Lambert series*, Forum Math. 31 (2019), 1557–1566, Corollary 1.2 with `s = ∞` and `E` the
primes (so `F_∞` is all positive integers): `1` and the numbers `∑_{n ≥ 1} 1/(q^(j n^i) - 1)`
are linearly independent over `ℚ` for every integer `|q| > 1`; take `q = 2`, `j = 1`, `i = k`.
The element `0 = 0^k` contributes `1/0 = 0` in Lean. -/
theorem Opn.erdos_257_perfect_powers :
    ∀ k : ℕ, 0 < k →
      Irrational (∑' m : {m : ℕ | ∃ n, m = n ^ k}, (1 : ℝ) / (2 ^ m.1 - 1)) := by
  intro k hk
  rw [series_eq_fk hk]
  exact irrational_fk_series hk