A rational series puts dilated tails near integers

spec-84446025 Opn.erdos_69_rational_dilated_tails_near_integers

proved

Proposed by a contributor.

$\displaystyle \frac{1}{T}\sum_{t=0}^{T-1}\Bigl\lvert q\,D_a(b+Qt) - \operatorname{round}\bigl(q\,D_a(b+Qt)\bigr)\Bigr\rvert \le q\sum_{p\mid a}\Bigl(\frac{1}{p}+\frac{1}{T}\Bigr),\qquad D_a(m) = \sum_{k=0}^{\infty}\frac{\omega\bigl(a(m+k+1)\bigr)}{2^{k+1}}$

For naturals q and an integer z with q·∑_{n≥0} ω(n)/2^n = z, and for naturals a, Q, b, T with a ≠ 0, T > 0 and every prime factor p of a coprime to Q, the average over t < T of the distance from q·D_a(b+Qt) to its nearest integer is at most q times the sum over the prime factors p of a of 1/p + 1/T. Everything is in ℝ: ω(n) is the number of distinct prime factors of n, round is Mathlib's rounding (half rounds up), the sum over p ∣ a runs over a.primeFactors, and each series is a tsum (0 when not summable).

unverified · history

Lean

theorem Opn.erdos_69_rational_dilated_tails_near_integers :
    ∀ (q : ℕ) (z : ℤ), (q : ℝ) * ∑' n : ℕ, (ω n : ℝ) / 2 ^ n = z →
      ∀ (a Q b T : ℕ), a ≠ 0 → 0 < T → (∀ p ∈ a.primeFactors, Nat.Coprime p Q) →
        (∑ t ∈ Finset.range T,
            |(q : ℝ) * ∑' k : ℕ, (ω (a * (b + Q * t + (k + 1))) : ℝ) / 2 ^ (k + 1)
              - round ((q : ℝ) * ∑' k : ℕ, (ω (a * (b + Q * t + (k + 1))) : ℝ) / 2 ^ (k + 1))|) / T
          ≤ (q : ℝ) * ∑ p ∈ a.primeFactors, ((1 : ℝ) / p + 1 / T) := by
  sorry

Why does it end in sorry?

A statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →

How it was proved

Proved by Proof.lean, checked by the kernel. Its attestation, 000315, records the gate’s run.

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000315.json, merge commit 612c41e635db.

Outline of Proof.lean, extracted by the gate at 82834c4684b8 from the proof’s elaboration: each step is a claim the proof establishes and the goal it leaves. Open a step for what it uses and its Lean lines.

hrat have ∀ (m : ℕ), ∃ (t : ℤ), (↑q : ℝ) * (∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (m + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) + ∑ p ∈ a.primeFactors, ∑' (k : ℕ), (if p ∣ m + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ))) = (↑t : ℝ)
Leaves (∑ t ∈ Finset.range T, |(↑q : ℝ) * ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (b + Q * t + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) - (↑(round ((↑q : ℝ) * ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (b + Q * t + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)))) : ℝ)|) / (↑T : ℝ) ≤ (↑q : ℝ) * ∑ p ∈ a.primeFactors, ((1 : ℝ) / (↑p : ℝ) + (1 : ℝ) / (↑T : ℝ)), with hrat : ∀ (m : ℕ), ∃ (t : ℤ), (↑q : ℝ) * (∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (m + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) + ∑ p ∈ a.primeFactors, ∑' (k : ℕ), (if p ∣ m + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ))) = (↑t : ℝ).
Uses library Exists.intro, Finset.range, sub_add_cancel.
Lean, lines 26–153
```
  have hrat : ∀ m : ℕ, ∃ t : ℤ,
      (q : ℝ) * (∑' k : ℕ, (ω (a * (m + (k + 1))) : ℝ) / 2 ^ (k + 1)
        + ∑ p ∈ a.primeFactors,
            ∑' k : ℕ, (if p ∣ m + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1)) = t := by
    intro m
    have hdil : ∑' k : ℕ, (ω (a * (m + (k + 1))) : ℝ) / 2 ^ (k + 1)
        = ∑' k : ℕ, (ω (m + (k + 1)) : ℝ) / 2 ^ (k + 1) + (ω a : ℝ)
          - ∑ p ∈ a.primeFactors,
              ∑' k : ℕ, (if p ∣ m + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1) := by
      -- ω is the number of prime factors
      have hω : ∀ x : ℕ, ω x = x.primeFactors.card := fun x => by
        rw [ArithmeticFunction.cardDistinctFactors_apply]; rfl
      -- the pointwise identity ω(a n) + #{p ∣ a : p ∣ n} = ω a + ω n
      have hpt : ∀ n : ℕ, n ≠ 0 →
          (ω (a * n) : ℝ) = (ω n : ℝ) + (ω a : ℝ)
            - ∑ p ∈ a.primeFactors, (if p ∣ n then (1 : ℝ) else 0) := by
        intro n hn
        have hu : (a * n).primeFactors = a.primeFactors ∪ n.primeFactors := Nat.primeFactors_mul ha hn
        have hi : a.primeFactors ∩ n.primeFactors = a.primeFactors.filter (· ∣ n) := by
          ext p
          simp only [Finset.mem_inter, Finset.mem_filter, Nat.mem_primeFactors]
          constructor
          · rintro ⟨h1, h2⟩; exact ⟨h1, h2.2.1⟩
          · rintro ⟨h1, h2⟩; exact ⟨h1, h1.1, h2, hn⟩
        have hc := Finset.card_union_add_card_inter a.primeFactors n.primeFactors
        rw [← hu, hi] at hc
        have hs : ∑ p ∈ a.primeFactors, (if p ∣ n then (1 : ℝ) else 0)
            = ((a.primeFactors.filter (· ∣ n)).card : ℝ) := by
          rw [Finset.sum_ite, Finset.sum_const_zero, add_zero, Finset.sum_const, nsmul_eq_mul, mul_one]
        rw [hs, hω, hω, hω]
        have hc' : ((a * n).primeFactors.card : ℝ) + ((a.primeFactors.filter (· ∣ n)).card : ℝ)
            = (a.primeFactors.card : ℝ) + (n.primeFactors.card : ℝ) := by exact_mod_cast hc
        linarith
      -- summability tools
      have hgeo : ∀ c : ℝ, Summable (fun k : ℕ => ((k : ℝ) + c) * (1 / 2 : ℝ) ^ k) := by
        intro c
        have h1 := summable_pow_mul_geometric_of_norm_lt_one 1 (by norm_num [Real.norm_eq_abs] : ‖(1 / 2 : ℝ)‖ < 1)
        have h2 := (summable_geometric_of_lt_one (by norm_num : (0 : ℝ) ≤ 1 / 2) (by norm_num)).mul_left c
        refine (h1.add h2).congr (fun k => ?_)
        simp only [pow_one]; ring
      have hw : ∀ k : ℕ, (1 : ℝ) / 2 ^ (k + 1) ≤ (1 / 2 : ℝ) ^ k := by
        intro k
        rw [one_div_pow, pow_succ]
        apply one_div_le_one_div_of_le (by positivity)
        linarith [pow_pos (by norm_num : (0 : ℝ) < 2) k]
      have hωle : ∀ x : ℕ, (ω x : ℝ) ≤ x + 1 := by
        intro x
        have h1 : ω x ≤ x + 1 := by
          rw [hω]
          calc x.primeFactors.card ≤ (Finset.range (x + 1)).card :=
                Finset.card_le_card (fun p hp =>
                  Finset.mem_range.2 (Nat.lt_succ_of_le (Nat.le_of_mem_primeFactors hp)))
            _ = x + 1 := Finset.card_range _
        exact_mod_cast h1
      have hS1 : Summable (fun k : ℕ => (ω (m + (k + 1)) : ℝ) / 2 ^ (k + 1)) := by
        refine Summable.of_nonneg_of_le (fun k => by positivity) (fun k => ?_) (hgeo ((m : ℝ) + 2))
        have h1 := hωle (m + (k + 1))
        have h2 := hw k
        have h3 : (0 : ℝ) ≤ (ω (m + (k + 1)) : ℝ) := by positivity
        calc (ω (m + (k + 1)) : ℝ) / 2 ^ (k + 1) = (ω (m + (k + 1)) : ℝ) * (1 / 2 ^ (k + 1)) := by ring
          _ ≤ ((k : ℝ) + ((m : ℝ) + 2)) * (1 / 2 : ℝ) ^ k := by
            apply mul_le_mul _ h2 (by positivity) (by positivity)
            push_cast at h1; linarith
      have hS2 : Summable (fun k : ℕ => (1 : ℝ) / 2 ^ (k + 1)) := by
        refine Summable.of_nonneg_of_le (fun k => by positivity) hw ?_
        exact summable_geometric_of_lt_one (by norm_num) (by norm_num)
      have hS3 : ∀ p : ℕ, Summable (fun k : ℕ => (if p ∣ m + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1)) := by
        intro p
        refine Summable.of_nonneg_of_le (fun k => by split_ifs <;> positivity) (fun k => ?_) hS2
        split_ifs <;> simp
      have hsum1 : ∑' k : ℕ, (1 : ℝ) / 2 ^ (k + 1) = 1 := by
        have : (fun k : ℕ => (1 : ℝ) / 2 ^ (k + 1)) = fun k => (1 / 2) * (1 / 2 : ℝ) ^ k := by
          funext k; rw [pow_succ, one_div_pow]; field_simp
        rw [this, tsum_mul_left, tsum_geometric_two]; norm_num
      -- assemble
      have hterm : ∀ k : ℕ, (ω (a * (m + (k + 1))) : ℝ) / 2 ^ (k + 1)
          = (ω (m + (k + 1)) : ℝ) / 2 ^ (k + 1) + (ω a : ℝ) * (1 / 2 ^ (k + 1))
            - ∑ p ∈ a.primeFactors, (if p ∣ m + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1) := by
        intro k
        rw [hpt (m + (k + 1)) (by omega), ← Finset.sum_div]
        ring
      rw [tsum_congr hterm, Summable.tsum_sub (hS1.add (hS2.mul_left _)) (summable_sum (fun p _ => hS3 p)),
        Summable.tsum_add hS1 (hS2.mul_left _), tsum_mul_left, hsum1, mul_one,
        Summable.tsum_finsetSum (fun p _ => hS3 p)]
    -- integrality of q times the plain tail
    have hbound : ∀ n : ℕ,
        (ω n : ℝ) / 2 ^ n ≤ (n : ℝ) ^ 1 * (1 / 2 : ℝ) ^ n + (1 / 2 : ℝ) ^ n := by
      intro n
      have h1 : ω n ≤ n + 1 := by
        rw [ArithmeticFunction.cardDistinctFactors_apply]
        calc n.primeFactorsList.dedup.length = n.primeFactors.card := rfl
          _ ≤ (Finset.range (n + 1)).card :=
              Finset.card_le_card (fun p hp =>
                Finset.mem_range.2 (Nat.lt_succ_of_le (Nat.le_of_mem_primeFactors hp)))
          _ = n + 1 := Finset.card_range _
      have h2 : (ω n : ℝ) ≤ (n : ℝ) + 1 := by exact_mod_cast h1
      have h4 : (0 : ℝ) ≤ ((2 : ℝ) ^ n)⁻¹ := by positivity
      rw [pow_one, one_div, inv_pow, div_eq_mul_inv]
      nlinarith [mul_le_mul_of_nonneg_right h2 h4]
    have hsum : Summable (fun n : ℕ => (ω n : ℝ) / 2 ^ n) := by
      refine Summable.of_nonneg_of_le (fun n => by positivity) hbound ?_
      exact (summable_pow_mul_geometric_of_norm_lt_one 1 (by norm_num [Real.norm_eq_abs])).add
        (summable_geometric_of_lt_one (by norm_num) (by norm_num))
    have htail : ∑' k : ℕ, (ω (m + (k + 1)) : ℝ) / 2 ^ (k + 1)
        = 2 ^ m * (∑' n : ℕ, (ω n : ℝ) / 2 ^ n
            - ∑ n ∈ Finset.range (m + 1), (ω n : ℝ) / 2 ^ n) := by
      have h := hsum.sum_add_tsum_nat_add (m + 1)
      have h2 : ∑' i : ℕ, (ω (i + (m + 1)) : ℝ) / 2 ^ (i + (m + 1))
          = (∑' k : ℕ, (ω (m + (k + 1)) : ℝ) / 2 ^ (k + 1)) / 2 ^ m := by
        rw [← tsum_div_const]
        refine tsum_congr (fun k => ?_)
        rw [show k + (m + 1) = m + (k + 1) by ring, show m + (k + 1) = (k + 1) + m by ring,
          pow_add, div_div]
      rw [h2] at h
      have h3 := eq_sub_of_add_eq' h
      rw [← h3]
      field_simp
    have hA : ∑ n ∈ Finset.range (m + 1), (q : ℝ) * (ω n : ℝ) * 2 ^ (m - n)
        = 2 ^ m * ((q : ℝ) * ∑ n ∈ Finset.range (m + 1), (ω n : ℝ) / 2 ^ n) := by
      rw [Finset.mul_sum, Finset.mul_sum]
      refine Finset.sum_congr rfl (fun n hn => ?_)
      have hn' : n ≤ m := Nat.lt_succ_iff.1 (Finset.mem_range.1 hn)
      rw [pow_sub₀ (2 : ℝ) two_ne_zero hn']
      field_simp
    refine ⟨2 ^ m * z - ∑ n ∈ Finset.range (m + 1), (q : ℤ) * ω n * 2 ^ (m - n) + q * ω a, ?_⟩
    push_cast
    rw [hdil, sub_add_cancel, htail]
    linear_combination (2 : ℝ) ^ m * hz + hA
```
targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 26–153 at 612c41e635db ↗
1. hrat.hdil have ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (m + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) = ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (m + (k + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) + (↑((ω : ℕ → ℕ) a) : ℝ) - ∑ p ∈ a.primeFactors, ∑' (k : ℕ), (if p ∣ m + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ))
  Leaves ∃ (t : ℤ), (↑q : ℝ) * (∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (m + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) + ∑ p ∈ a.primeFactors, ∑' (k : ℕ), (if p ∣ m + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ))) = (↑t : ℝ), with hdil : ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (m + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) = ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (m + (k + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) + (↑((ω : ℕ → ℕ) a) : ℝ) - ∑ p ∈ a.primeFactors, ∑' (k : ℕ), (if p ∣ m + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)).
  Uses library tsum_congr, Summable.tsum_sub, summable_sum, Summable.tsum_add, tsum_mul_left, mul_one, Summable.tsum_finsetSum.
  Lean, lines 31–109
  have hdil : ∑' k : ℕ, (ω (a * (m + (k + 1))) : ℝ) / 2 ^ (k + 1) = ∑' k : ℕ, (ω (m + (k + 1)) : ℝ) / 2 ^ (k + 1) + (ω a : ℝ) - ∑ p ∈ a.primeFactors, ∑' k : ℕ, (if p ∣ m + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1) := by -- ω is the number of prime factors have hω : ∀ x : ℕ, ω x = x.primeFactors.card := fun x => by rw [ArithmeticFunction.cardDistinctFactors_apply]; rfl -- the pointwise identity ω(a n) + #{p ∣ a : p ∣ n} = ω a + ω n have hpt : ∀ n : ℕ, n ≠ 0 → (ω (a * n) : ℝ) = (ω n : ℝ) + (ω a : ℝ) - ∑ p ∈ a.primeFactors, (if p ∣ n then (1 : ℝ) else 0) := by intro n hn have hu : (a * n).primeFactors = a.primeFactors ∪ n.primeFactors := Nat.primeFactors_mul ha hn have hi : a.primeFactors ∩ n.primeFactors = a.primeFactors.filter (· ∣ n) := by ext p simp only [Finset.mem_inter, Finset.mem_filter, Nat.mem_primeFactors] constructor · rintro ⟨h1, h2⟩; exact ⟨h1, h2.2.1⟩ · rintro ⟨h1, h2⟩; exact ⟨h1, h1.1, h2, hn⟩ have hc := Finset.card_union_add_card_inter a.primeFactors n.primeFactors rw [← hu, hi] at hc have hs : ∑ p ∈ a.primeFactors, (if p ∣ n then (1 : ℝ) else 0) = ((a.primeFactors.filter (· ∣ n)).card : ℝ) := by rw [Finset.sum_ite, Finset.sum_const_zero, add_zero, Finset.sum_const, nsmul_eq_mul, mul_one] rw [hs, hω, hω, hω] have hc' : ((a * n).primeFactors.card : ℝ) + ((a.primeFactors.filter (· ∣ n)).card : ℝ) = (a.primeFactors.card : ℝ) + (n.primeFactors.card : ℝ) := by exact_mod_cast hc linarith -- summability tools have hgeo : ∀ c : ℝ, Summable (fun k : ℕ => ((k : ℝ) + c) * (1 / 2 : ℝ) ^ k) := by intro c have h1 := summable_pow_mul_geometric_of_norm_lt_one 1 (by norm_num [Real.norm_eq_abs] : ‖(1 / 2 : ℝ)‖ < 1) have h2 := (summable_geometric_of_lt_one (by norm_num : (0 : ℝ) ≤ 1 / 2) (by norm_num)).mul_left c refine (h1.add h2).congr (fun k => ?_) simp only [pow_one]; ring have hw : ∀ k : ℕ, (1 : ℝ) / 2 ^ (k + 1) ≤ (1 / 2 : ℝ) ^ k := by intro k rw [one_div_pow, pow_succ] apply one_div_le_one_div_of_le (by positivity) linarith [pow_pos (by norm_num : (0 : ℝ) < 2) k] have hωle : ∀ x : ℕ, (ω x : ℝ) ≤ x + 1 := by intro x have h1 : ω x ≤ x + 1 := by rw [hω] calc x.primeFactors.card ≤ (Finset.range (x + 1)).card := Finset.card_le_card (fun p hp => Finset.mem_range.2 (Nat.lt_succ_of_le (Nat.le_of_mem_primeFactors hp))) _ = x + 1 := Finset.card_range _ exact_mod_cast h1 have hS1 : Summable (fun k : ℕ => (ω (m + (k + 1)) : ℝ) / 2 ^ (k + 1)) := by refine Summable.of_nonneg_of_le (fun k => by positivity) (fun k => ?_) (hgeo ((m : ℝ) + 2)) have h1 := hωle (m + (k + 1)) have h2 := hw k have h3 : (0 : ℝ) ≤ (ω (m + (k + 1)) : ℝ) := by positivity calc (ω (m + (k + 1)) : ℝ) / 2 ^ (k + 1) = (ω (m + (k + 1)) : ℝ) * (1 / 2 ^ (k + 1)) := by ring _ ≤ ((k : ℝ) + ((m : ℝ) + 2)) * (1 / 2 : ℝ) ^ k := by apply mul_le_mul _ h2 (by positivity) (by positivity) push_cast at h1; linarith have hS2 : Summable (fun k : ℕ => (1 : ℝ) / 2 ^ (k + 1)) := by refine Summable.of_nonneg_of_le (fun k => by positivity) hw ?_ exact summable_geometric_of_lt_one (by norm_num) (by norm_num) have hS3 : ∀ p : ℕ, Summable (fun k : ℕ => (if p ∣ m + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1)) := by intro p refine Summable.of_nonneg_of_le (fun k => by split_ifs <;> positivity) (fun k => ?_) hS2 split_ifs <;> simp have hsum1 : ∑' k : ℕ, (1 : ℝ) / 2 ^ (k + 1) = 1 := by have : (fun k : ℕ => (1 : ℝ) / 2 ^ (k + 1)) = fun k => (1 / 2) * (1 / 2 : ℝ) ^ k := by funext k; rw [pow_succ, one_div_pow]; field_simp rw [this, tsum_mul_left, tsum_geometric_two]; norm_num -- assemble have hterm : ∀ k : ℕ, (ω (a * (m + (k + 1))) : ℝ) / 2 ^ (k + 1) = (ω (m + (k + 1)) : ℝ) / 2 ^ (k + 1) + (ω a : ℝ) * (1 / 2 ^ (k + 1)) - ∑ p ∈ a.primeFactors, (if p ∣ m + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1) := by intro k rw [hpt (m + (k + 1)) (by omega), ← Finset.sum_div] ring rw [tsum_congr hterm, Summable.tsum_sub (hS1.add (hS2.mul_left _)) (summable_sum (fun p _ => hS3 p)), Summable.tsum_add hS1 (hS2.mul_left _), tsum_mul_left, hsum1, mul_one, Summable.tsum_finsetSum (fun p _ => hS3 p)]
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 31–109 at 612c41e635db ↗
  hrat.hdil.h_x3c9 (hω) have ∀ (x : ℕ), (ω : ℕ → ℕ) x = x.primeFactors.card
  Leaves ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (m + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) = ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (m + (k + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) + (↑((ω : ℕ → ℕ) a) : ℝ) - ∑ p ∈ a.primeFactors, ∑' (k : ℕ), (if p ∣ m + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)), with hω : ∀ (x : ℕ), (ω : ℕ → ℕ) x = x.primeFactors.card.
  Uses library ArithmeticFunction.cardDistinctFactors_apply.
  Lean, lines 36–37
  have hω : ∀ x : ℕ, ω x = x.primeFactors.card := fun x => by rw [ArithmeticFunction.cardDistinctFactors_apply]; rfl
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 36–37 at 612c41e635db ↗
  hrat.hdil.hpt have ∀ (n : ℕ), n ≠ (0 : ℕ) → (↑((ω : ℕ → ℕ) (a * n)) : ℝ) = (↑((ω : ℕ → ℕ) n) : ℝ) + (↑((ω : ℕ → ℕ) a) : ℝ) - ∑ p ∈ a.primeFactors, if p ∣ n then (1 : ℝ) else (0 : ℝ)
  Leaves ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (m + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) = ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (m + (k + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) + (↑((ω : ℕ → ℕ) a) : ℝ) - ∑ p ∈ a.primeFactors, ∑' (k : ℕ), (if p ∣ m + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)), with hpt : ∀ (n : ℕ), n ≠ (0 : ℕ) → (↑((ω : ℕ → ℕ) (a * n)) : ℝ) = (↑((ω : ℕ → ℕ) n) : ℝ) + (↑((ω : ℕ → ℕ) a) : ℝ) - ∑ p ∈ a.primeFactors, if p ∣ n then (1 : ℝ) else (0 : ℝ).
  Lean, lines 39–58
  have hpt : ∀ n : ℕ, n ≠ 0 → (ω (a * n) : ℝ) = (ω n : ℝ) + (ω a : ℝ) - ∑ p ∈ a.primeFactors, (if p ∣ n then (1 : ℝ) else 0) := by intro n hn have hu : (a * n).primeFactors = a.primeFactors ∪ n.primeFactors := Nat.primeFactors_mul ha hn have hi : a.primeFactors ∩ n.primeFactors = a.primeFactors.filter (· ∣ n) := by ext p simp only [Finset.mem_inter, Finset.mem_filter, Nat.mem_primeFactors] constructor · rintro ⟨h1, h2⟩; exact ⟨h1, h2.2.1⟩ · rintro ⟨h1, h2⟩; exact ⟨h1, h1.1, h2, hn⟩ have hc := Finset.card_union_add_card_inter a.primeFactors n.primeFactors rw [← hu, hi] at hc have hs : ∑ p ∈ a.primeFactors, (if p ∣ n then (1 : ℝ) else 0) = ((a.primeFactors.filter (· ∣ n)).card : ℝ) := by rw [Finset.sum_ite, Finset.sum_const_zero, add_zero, Finset.sum_const, nsmul_eq_mul, mul_one] rw [hs, hω, hω, hω] have hc' : ((a * n).primeFactors.card : ℝ) + ((a.primeFactors.filter (· ∣ n)).card : ℝ) = (a.primeFactors.card : ℝ) + (n.primeFactors.card : ℝ) := by exact_mod_cast hc linarith
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 39–58 at 612c41e635db ↗
  hrat.hdil.hpt.hu have (a * n).primeFactors = a.primeFactors ∪ n.primeFactors
  Leaves (↑((ω : ℕ → ℕ) (a * n)) : ℝ) = (↑((ω : ℕ → ℕ) n) : ℝ) + (↑((ω : ℕ → ℕ) a) : ℝ) - ∑ p ∈ a.primeFactors, if p ∣ n then (1 : ℝ) else (0 : ℝ), with hu : (a * n).primeFactors = a.primeFactors ∪ n.primeFactors.
  Uses library Nat.primeFactors_mul.
  Lean, line 43
  have hu : (a * n).primeFactors = a.primeFactors ∪ n.primeFactors := Nat.primeFactors_mul ha hn
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 43 at 612c41e635db ↗
  hrat.hdil.hpt.hi have a.primeFactors ∩ n.primeFactors = {x ∈ a.primeFactors | x ∣ n}
  Leaves (↑((ω : ℕ → ℕ) (a * n)) : ℝ) = (↑((ω : ℕ → ℕ) n) : ℝ) + (↑((ω : ℕ → ℕ) a) : ℝ) - ∑ p ∈ a.primeFactors, if p ∣ n then (1 : ℝ) else (0 : ℝ), with hi : a.primeFactors ∩ n.primeFactors = {x ∈ a.primeFactors | x ∣ n}.
  Uses library Finset.mem_inter, Finset.mem_filter, Nat.mem_primeFactors.
  Lean, lines 44–49
  have hi : a.primeFactors ∩ n.primeFactors = a.primeFactors.filter (· ∣ n) := by ext p simp only [Finset.mem_inter, Finset.mem_filter, Nat.mem_primeFactors] constructor · rintro ⟨h1, h2⟩; exact ⟨h1, h2.2.1⟩ · rintro ⟨h1, h2⟩; exact ⟨h1, h1.1, h2, hn⟩
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 44–49 at 612c41e635db ↗
  hrat.hdil.hpt.hi.s1 case
  Leaves (Nat.Prime p ∧ p ∣ a ∧ a ≠ (0 : ℕ)) ∧ Nat.Prime p ∧ p ∣ n ∧ n ≠ (0 : ℕ) → (Nat.Prime p ∧ p ∣ a ∧ a ≠ (0 : ℕ)) ∧ p ∣ n.
  Uses library And.intro.
  Lean, line 48
  · rintro ⟨h1, h2⟩; exact ⟨h1, h2.2.1⟩
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 48 at 612c41e635db ↗
  hrat.hdil.hpt.hi.s2 case
  Leaves (Nat.Prime p ∧ p ∣ a ∧ a ≠ (0 : ℕ)) ∧ p ∣ n → (Nat.Prime p ∧ p ∣ a ∧ a ≠ (0 : ℕ)) ∧ Nat.Prime p ∧ p ∣ n ∧ n ≠ (0 : ℕ).
  Uses library And.intro.
  Lean, line 49
  · rintro ⟨h1, h2⟩; exact ⟨h1, h1.1, h2, hn⟩
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 49 at 612c41e635db ↗
  hrat.hdil.hpt.hc have (a.primeFactors ∪ n.primeFactors).card + (a.primeFactors ∩ n.primeFactors).card = a.primeFactors.card + n.primeFactors.card
  Leaves (↑((ω : ℕ → ℕ) (a * n)) : ℝ) = (↑((ω : ℕ → ℕ) n) : ℝ) + (↑((ω : ℕ → ℕ) a) : ℝ) - ∑ p ∈ a.primeFactors, if p ∣ n then (1 : ℝ) else (0 : ℝ), with hc : (a.primeFactors ∪ n.primeFactors).card + (a.primeFactors ∩ n.primeFactors).card = a.primeFactors.card + n.primeFactors.card.
  Uses library Finset.card_union_add_card_inter.
  Lean, line 50
  have hc := Finset.card_union_add_card_inter a.primeFactors n.primeFactors
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 50 at 612c41e635db ↗
  hrat.hdil.hpt.hs have (∑ p ∈ a.primeFactors, if p ∣ n then (1 : ℝ) else (0 : ℝ)) = (↑{x ∈ a.primeFactors | x ∣ n}.card : ℝ)
  Leaves (↑((ω : ℕ → ℕ) (a * n)) : ℝ) = (↑((ω : ℕ → ℕ) n) : ℝ) + (↑((ω : ℕ → ℕ) a) : ℝ) - ∑ p ∈ a.primeFactors, if p ∣ n then (1 : ℝ) else (0 : ℝ), with hs : (∑ p ∈ a.primeFactors, if p ∣ n then (1 : ℝ) else (0 : ℝ)) = (↑{x ∈ a.primeFactors | x ∣ n}.card : ℝ).
  Uses library Finset.sum_ite, Finset.sum_const_zero, add_zero, Finset.sum_const, nsmul_eq_mul, mul_one.
  Lean, lines 52–54
  have hs : ∑ p ∈ a.primeFactors, (if p ∣ n then (1 : ℝ) else 0) = ((a.primeFactors.filter (· ∣ n)).card : ℝ) := by rw [Finset.sum_ite, Finset.sum_const_zero, add_zero, Finset.sum_const, nsmul_eq_mul, mul_one]
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 52–54 at 612c41e635db ↗
  hrat.hdil.hpt.hc' have (↑(a * n).primeFactors.card : ℝ) + (↑{x ∈ a.primeFactors | x ∣ n}.card : ℝ) = (↑a.primeFactors.card : ℝ) + (↑n.primeFactors.card : ℝ)
  Leaves (↑(a * n).primeFactors.card : ℝ) = (↑n.primeFactors.card : ℝ) + (↑a.primeFactors.card : ℝ) - (↑{x ∈ a.primeFactors | x ∣ n}.card : ℝ), with hc' : (↑(a * n).primeFactors.card : ℝ) + (↑{x ∈ a.primeFactors | x ∣ n}.card : ℝ) = (↑a.primeFactors.card : ℝ) + (↑n.primeFactors.card : ℝ).
  Lean, lines 56–57
  have hc' : ((a * n).primeFactors.card : ℝ) + ((a.primeFactors.filter (· ∣ n)).card : ℝ) = (a.primeFactors.card : ℝ) + (n.primeFactors.card : ℝ) := by exact_mod_cast hc
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 56–57 at 612c41e635db ↗
  hrat.hdil.hgeo have ∀ (c : ℝ), Summable fun (k : ℕ) => ((↑k : ℝ) + c) * (1 / 2 : ℝ) ^ k
  Leaves ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (m + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) = ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (m + (k + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) + (↑((ω : ℕ → ℕ) a) : ℝ) - ∑ p ∈ a.primeFactors, ∑' (k : ℕ), (if p ∣ m + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)), with hgeo : ∀ (c : ℝ), Summable fun (k : ℕ) => ((↑k : ℝ) + c) * (1 / 2 : ℝ) ^ k.
  Uses library Summable, pow_one.
  Lean, lines 60–65
  have hgeo : ∀ c : ℝ, Summable (fun k : ℕ => ((k : ℝ) + c) * (1 / 2 : ℝ) ^ k) := by intro c have h1 := summable_pow_mul_geometric_of_norm_lt_one 1 (by norm_num [Real.norm_eq_abs] : ‖(1 / 2 : ℝ)‖ < 1) have h2 := (summable_geometric_of_lt_one (by norm_num : (0 : ℝ) ≤ 1 / 2) (by norm_num)).mul_left c refine (h1.add h2).congr (fun k => ?_) simp only [pow_one]; ring
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 60–65 at 612c41e635db ↗
  hrat.hdil.hgeo.h1 have Summable fun (n : ℕ) => (↑n : ℝ) ^ (1 : ℕ) * (1 / 2 : ℝ) ^ n
  Leaves Summable fun (k : ℕ) => ((↑k : ℝ) + c) * (1 / 2 : ℝ) ^ k, with h1 : Summable fun (n : ℕ) => (↑n : ℝ) ^ (1 : ℕ) * (1 / 2 : ℝ) ^ n.
  Uses library summable_pow_mul_geometric_of_norm_lt_one, Real.norm_eq_abs.
  Lean, line 62
  have h1 := summable_pow_mul_geometric_of_norm_lt_one 1 (by norm_num [Real.norm_eq_abs] : ‖(1 / 2 : ℝ)‖ < 1)
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 62 at 612c41e635db ↗
  hrat.hdil.hgeo.h2 have Summable fun (i : ℕ) => c * (1 / 2 : ℝ) ^ i
  Leaves Summable fun (k : ℕ) => ((↑k : ℝ) + c) * (1 / 2 : ℝ) ^ k, with h2 : Summable fun (i : ℕ) => c * (1 / 2 : ℝ) ^ i.
  Uses library summable_geometric_of_lt_one.
  Lean, line 63
  have h2 := (summable_geometric_of_lt_one (by norm_num : (0 : ℝ) ≤ 1 / 2) (by norm_num)).mul_left c
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 63 at 612c41e635db ↗
  hrat.hdil.hw have ∀ (k : ℕ), (1 : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) ≤ (1 / 2 : ℝ) ^ k
  Leaves ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (m + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) = ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (m + (k + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) + (↑((ω : ℕ → ℕ) a) : ℝ) - ∑ p ∈ a.primeFactors, ∑' (k : ℕ), (if p ∣ m + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)), with hw : ∀ (k : ℕ), (1 : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) ≤ (1 / 2 : ℝ) ^ k.
  Uses library one_div_pow, pow_succ, one_div_le_one_div_of_le, pow_pos.
  Lean, lines 66–70
  have hw : ∀ k : ℕ, (1 : ℝ) / 2 ^ (k + 1) ≤ (1 / 2 : ℝ) ^ k := by intro k rw [one_div_pow, pow_succ] apply one_div_le_one_div_of_le (by positivity) linarith [pow_pos (by norm_num : (0 : ℝ) < 2) k]
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 66–70 at 612c41e635db ↗
  hrat.hdil.h_x3c9le (hωle) have ∀ (x : ℕ), (↑((ω : ℕ → ℕ) x) : ℝ) ≤ (↑x : ℝ) + (1 : ℝ)
  Leaves ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (m + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) = ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (m + (k + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) + (↑((ω : ℕ → ℕ) a) : ℝ) - ∑ p ∈ a.primeFactors, ∑' (k : ℕ), (if p ∣ m + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)), with hωle : ∀ (x : ℕ), (↑((ω : ℕ → ℕ) x) : ℝ) ≤ (↑x : ℝ) + (1 : ℝ).
  Lean, lines 71–79
  have hωle : ∀ x : ℕ, (ω x : ℝ) ≤ x + 1 := by intro x have h1 : ω x ≤ x + 1 := by rw [hω] calc x.primeFactors.card ≤ (Finset.range (x + 1)).card := Finset.card_le_card (fun p hp => Finset.mem_range.2 (Nat.lt_succ_of_le (Nat.le_of_mem_primeFactors hp))) _ = x + 1 := Finset.card_range _ exact_mod_cast h1
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 71–79 at 612c41e635db ↗
  hrat.hdil.h_x3c9le.h1 have (ω : ℕ → ℕ) x ≤ x + (1 : ℕ)
  Leaves (↑((ω : ℕ → ℕ) x) : ℝ) ≤ (↑x : ℝ) + (1 : ℝ), with h1 : (ω : ℕ → ℕ) x ≤ x + (1 : ℕ).
  Lean, lines 73–78
  have h1 : ω x ≤ x + 1 := by rw [hω] calc x.primeFactors.card ≤ (Finset.range (x + 1)).card := Finset.card_le_card (fun p hp => Finset.mem_range.2 (Nat.lt_succ_of_le (Nat.le_of_mem_primeFactors hp))) _ = x + 1 := Finset.card_range _
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 73–78 at 612c41e635db ↗
  hrat.hdil.h_x3c9le.h1.s1 calc x.primeFactors.card ≤ (Finset.range (x + (1 : ℕ))).card
  Closes the goal.
  Uses library Finset.range, Finset.card_le_card, Finset.mem_range, Nat.lt_succ_of_le, Nat.le_of_mem_primeFactors.
  Lean, lines 75–77
  calc x.primeFactors.card ≤ (Finset.range (x + 1)).card := Finset.card_le_card (fun p hp => Finset.mem_range.2 (Nat.lt_succ_of_le (Nat.le_of_mem_primeFactors hp)))
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 75–77 at 612c41e635db ↗
  hrat.hdil.h_x3c9le.h1.s2 calc (Finset.range (x + (1 : ℕ))).card = x + (1 : ℕ)
  Closes the goal.
  Uses library Finset.card_range.
  Lean, line 78
  _ = x + 1 := Finset.card_range _
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 78 at 612c41e635db ↗
  hrat.hdil.hS1 have Summable fun (k : ℕ) => (↑((ω : ℕ → ℕ) (m + (k + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ))
  Leaves ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (m + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) = ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (m + (k + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) + (↑((ω : ℕ → ℕ) a) : ℝ) - ∑ p ∈ a.primeFactors, ∑' (k : ℕ), (if p ∣ m + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)), with hS1 : Summable fun (k : ℕ) => (↑((ω : ℕ → ℕ) (m + (k + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)).
  Uses library Summable, Summable.of_nonneg_of_le.
  Lean, lines 80–88
  have hS1 : Summable (fun k : ℕ => (ω (m + (k + 1)) : ℝ) / 2 ^ (k + 1)) := by refine Summable.of_nonneg_of_le (fun k => by positivity) (fun k => ?_) (hgeo ((m : ℝ) + 2)) have h1 := hωle (m + (k + 1)) have h2 := hw k have h3 : (0 : ℝ) ≤ (ω (m + (k + 1)) : ℝ) := by positivity calc (ω (m + (k + 1)) : ℝ) / 2 ^ (k + 1) = (ω (m + (k + 1)) : ℝ) * (1 / 2 ^ (k + 1)) := by ring _ ≤ ((k : ℝ) + ((m : ℝ) + 2)) * (1 / 2 : ℝ) ^ k := by apply mul_le_mul _ h2 (by positivity) (by positivity) push_cast at h1; linarith
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 80–88 at 612c41e635db ↗
  hrat.hdil.hS1.h1 have (↑((ω : ℕ → ℕ) (m + (k + (1 : ℕ)))) : ℝ) ≤ (↑(m + (k + (1 : ℕ))) : ℝ) + (1 : ℝ)
  Leaves (↑((ω : ℕ → ℕ) (m + (k + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) ≤ ((↑k : ℝ) + ((↑m : ℝ) + (2 : ℝ))) * (1 / 2 : ℝ) ^ k, with h1 : (↑((ω : ℕ → ℕ) (m + (k + (1 : ℕ)))) : ℝ) ≤ (↑(m + (k + (1 : ℕ))) : ℝ) + (1 : ℝ).
  Lean, line 82
  have h1 := hωle (m + (k + 1))
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 82 at 612c41e635db ↗
  hrat.hdil.hS1.h2 have (1 : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) ≤ (1 / 2 : ℝ) ^ k
  Leaves (↑((ω : ℕ → ℕ) (m + (k + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) ≤ ((↑k : ℝ) + ((↑m : ℝ) + (2 : ℝ))) * (1 / 2 : ℝ) ^ k, with h2 : (1 : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) ≤ (1 / 2 : ℝ) ^ k.
  Lean, line 83
  have h2 := hw k
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 83 at 612c41e635db ↗
  hrat.hdil.hS1.h3 have (0 : ℝ) ≤ (↑((ω : ℕ → ℕ) (m + (k + (1 : ℕ)))) : ℝ) routine: positivity
  Leaves (↑((ω : ℕ → ℕ) (m + (k + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) ≤ ((↑k : ℝ) + ((↑m : ℝ) + (2 : ℝ))) * (1 / 2 : ℝ) ^ k, with h3 : (0 : ℝ) ≤ (↑((ω : ℕ → ℕ) (m + (k + (1 : ℕ)))) : ℝ).
  Lean, line 84
  have h3 : (0 : ℝ) ≤ (ω (m + (k + 1)) : ℝ) := by positivity
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 84 at 612c41e635db ↗
  hrat.hdil.hS1.s4 calc (↑((ω : ℕ → ℕ) (m + (k + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) = (↑((ω : ℕ → ℕ) (m + (k + (1 : ℕ)))) : ℝ) * ((1 : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ))) routine: ring
  Closes the goal.
  Lean, line 85
  calc (ω (m + (k + 1)) : ℝ) / 2 ^ (k + 1) = (ω (m + (k + 1)) : ℝ) * (1 / 2 ^ (k + 1)) := by ring
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 85 at 612c41e635db ↗
  hrat.hdil.hS1.s5 calc
  Closes the goal.
  Uses library mul_le_mul.
  Lean, lines 86–88
  _ ≤ ((k : ℝ) + ((m : ℝ) + 2)) * (1 / 2 : ℝ) ^ k := by apply mul_le_mul _ h2 (by positivity) (by positivity) push_cast at h1; linarith
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 86–88 at 612c41e635db ↗
  hrat.hdil.hS2 have Summable fun (k : ℕ) => (1 : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ))
  Leaves ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (m + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) = ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (m + (k + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) + (↑((ω : ℕ → ℕ) a) : ℝ) - ∑ p ∈ a.primeFactors, ∑' (k : ℕ), (if p ∣ m + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)), with hS2 : Summable fun (k : ℕ) => (1 : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)).
  Uses library Summable, Summable.of_nonneg_of_le, summable_geometric_of_lt_one.
  Lean, lines 89–91
  have hS2 : Summable (fun k : ℕ => (1 : ℝ) / 2 ^ (k + 1)) := by refine Summable.of_nonneg_of_le (fun k => by positivity) hw ?_ exact summable_geometric_of_lt_one (by norm_num) (by norm_num)
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 89–91 at 612c41e635db ↗
  hrat.hdil.hS3 have ∀ (p : ℕ), Summable fun (k : ℕ) => (if p ∣ m + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ))
  Leaves ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (m + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) = ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (m + (k + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) + (↑((ω : ℕ → ℕ) a) : ℝ) - ∑ p ∈ a.primeFactors, ∑' (k : ℕ), (if p ∣ m + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)), with hS3 : ∀ (p : ℕ), Summable fun (k : ℕ) => (if p ∣ m + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)).
  Uses library Summable, Summable.of_nonneg_of_le.
  Lean, lines 92–95
  have hS3 : ∀ p : ℕ, Summable (fun k : ℕ => (if p ∣ m + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1)) := by intro p refine Summable.of_nonneg_of_le (fun k => by split_ifs <;> positivity) (fun k => ?_) hS2 split_ifs <;> simp
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 92–95 at 612c41e635db ↗
  hrat.hdil.hsum1 have ∑' (k : ℕ), (1 : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) = (1 : ℝ)
  Leaves ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (m + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) = ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (m + (k + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) + (↑((ω : ℕ → ℕ) a) : ℝ) - ∑ p ∈ a.primeFactors, ∑' (k : ℕ), (if p ∣ m + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)), with hsum1 : ∑' (k : ℕ), (1 : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) = (1 : ℝ).
  Uses library tsum_mul_left, tsum_geometric_two.
  Lean, lines 96–99
  have hsum1 : ∑' k : ℕ, (1 : ℝ) / 2 ^ (k + 1) = 1 := by have : (fun k : ℕ => (1 : ℝ) / 2 ^ (k + 1)) = fun k => (1 / 2) * (1 / 2 : ℝ) ^ k := by funext k; rw [pow_succ, one_div_pow]; field_simp rw [this, tsum_mul_left, tsum_geometric_two]; norm_num
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 96–99 at 612c41e635db ↗
  hrat.hdil.hsum1.this have (fun (k : ℕ) => (1 : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ))) = fun (k : ℕ) => (1 / 2 : ℝ) * (1 / 2 : ℝ) ^ k
  Leaves ∑' (k : ℕ), (1 : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) = (1 : ℝ), with this : (fun (k : ℕ) => (1 : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ))) = fun (k : ℕ) => (1 / 2 : ℝ) * (1 / 2 : ℝ) ^ k.
  Uses library pow_succ, one_div_pow.
  Lean, lines 97–98
  have : (fun k : ℕ => (1 : ℝ) / 2 ^ (k + 1)) = fun k => (1 / 2) * (1 / 2 : ℝ) ^ k := by funext k; rw [pow_succ, one_div_pow]; field_simp
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 97–98 at 612c41e635db ↗
  hrat.hdil.hterm have ∀ (k : ℕ), (↑((ω : ℕ → ℕ) (a * (m + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) = (↑((ω : ℕ → ℕ) (m + (k + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) + (↑((ω : ℕ → ℕ) a) : ℝ) * ((1 : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ))) - ∑ p ∈ a.primeFactors, (if p ∣ m + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ))
  Leaves ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (m + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) = ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (m + (k + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) + (↑((ω : ℕ → ℕ) a) : ℝ) - ∑ p ∈ a.primeFactors, ∑' (k : ℕ), (if p ∣ m + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)), with hterm : ∀ (k : ℕ), (↑((ω : ℕ → ℕ) (a * (m + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) = (↑((ω : ℕ → ℕ) (m + (k + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) + (↑((ω : ℕ → ℕ) a) : ℝ) * ((1 : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ))) - ∑ p ∈ a.primeFactors, (if p ∣ m + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)).
  Uses library Finset.sum_div.
  Lean, lines 101–106
  have hterm : ∀ k : ℕ, (ω (a * (m + (k + 1))) : ℝ) / 2 ^ (k + 1) = (ω (m + (k + 1)) : ℝ) / 2 ^ (k + 1) + (ω a : ℝ) * (1 / 2 ^ (k + 1)) - ∑ p ∈ a.primeFactors, (if p ∣ m + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1) := by intro k rw [hpt (m + (k + 1)) (by omega), ← Finset.sum_div] ring
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 101–106 at 612c41e635db ↗
2. hrat.hbound have ∀ (n : ℕ), (↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n ≤ (↑n : ℝ) ^ (1 : ℕ) * (1 / 2 : ℝ) ^ n + (1 / 2 : ℝ) ^ n
  Leaves ∃ (t : ℤ), (↑q : ℝ) * (∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (m + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) + ∑ p ∈ a.primeFactors, ∑' (k : ℕ), (if p ∣ m + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ))) = (↑t : ℝ), with hbound : ∀ (n : ℕ), (↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n ≤ (↑n : ℝ) ^ (1 : ℕ) * (1 / 2 : ℝ) ^ n + (1 / 2 : ℝ) ^ n.
  Uses library pow_one, one_div, inv_pow, div_eq_mul_inv, mul_le_mul_of_nonneg_right.
  Lean, lines 111–124
  have hbound : ∀ n : ℕ, (ω n : ℝ) / 2 ^ n ≤ (n : ℝ) ^ 1 * (1 / 2 : ℝ) ^ n + (1 / 2 : ℝ) ^ n := by intro n have h1 : ω n ≤ n + 1 := by rw [ArithmeticFunction.cardDistinctFactors_apply] calc n.primeFactorsList.dedup.length = n.primeFactors.card := rfl _ ≤ (Finset.range (n + 1)).card := Finset.card_le_card (fun p hp => Finset.mem_range.2 (Nat.lt_succ_of_le (Nat.le_of_mem_primeFactors hp))) _ = n + 1 := Finset.card_range _ have h2 : (ω n : ℝ) ≤ (n : ℝ) + 1 := by exact_mod_cast h1 have h4 : (0 : ℝ) ≤ ((2 : ℝ) ^ n)⁻¹ := by positivity rw [pow_one, one_div, inv_pow, div_eq_mul_inv] nlinarith [mul_le_mul_of_nonneg_right h2 h4]
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 111–124 at 612c41e635db ↗
  hrat.hbound.h1 have (ω : ℕ → ℕ) n ≤ n + (1 : ℕ)
  Leaves (↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n ≤ (↑n : ℝ) ^ (1 : ℕ) * (1 / 2 : ℝ) ^ n + (1 / 2 : ℝ) ^ n, with h1 : (ω : ℕ → ℕ) n ≤ n + (1 : ℕ).
  Uses library ArithmeticFunction.cardDistinctFactors_apply.
  Lean, lines 114–120
  have h1 : ω n ≤ n + 1 := by rw [ArithmeticFunction.cardDistinctFactors_apply] calc n.primeFactorsList.dedup.length = n.primeFactors.card := rfl _ ≤ (Finset.range (n + 1)).card := Finset.card_le_card (fun p hp => Finset.mem_range.2 (Nat.lt_succ_of_le (Nat.le_of_mem_primeFactors hp))) _ = n + 1 := Finset.card_range _
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 114–120 at 612c41e635db ↗
  hrat.hbound.h1.s1 calc n.primeFactorsList.dedup.length = n.primeFactors.card
  Closes the goal.
  Uses library rfl.
  Lean, line 116
  calc n.primeFactorsList.dedup.length = n.primeFactors.card := rfl
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 116 at 612c41e635db ↗
  hrat.hbound.h1.s2 calc n.primeFactors.card ≤ (Finset.range (n + (1 : ℕ))).card
  Closes the goal.
  Uses library Finset.range, Finset.card_le_card, Finset.mem_range, Nat.lt_succ_of_le, Nat.le_of_mem_primeFactors.
  Lean, lines 117–119
  _ ≤ (Finset.range (n + 1)).card := Finset.card_le_card (fun p hp => Finset.mem_range.2 (Nat.lt_succ_of_le (Nat.le_of_mem_primeFactors hp)))
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 117–119 at 612c41e635db ↗
  hrat.hbound.h1.s3 calc (Finset.range (n + (1 : ℕ))).card = n + (1 : ℕ)
  Closes the goal.
  Uses library Finset.card_range.
  Lean, line 120
  _ = n + 1 := Finset.card_range _
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 120 at 612c41e635db ↗
  hrat.hbound.h2 have (↑((ω : ℕ → ℕ) n) : ℝ) ≤ (↑n : ℝ) + (1 : ℝ)
  Leaves (↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n ≤ (↑n : ℝ) ^ (1 : ℕ) * (1 / 2 : ℝ) ^ n + (1 / 2 : ℝ) ^ n, with h2 : (↑((ω : ℕ → ℕ) n) : ℝ) ≤ (↑n : ℝ) + (1 : ℝ).
  Lean, line 121
  have h2 : (ω n : ℝ) ≤ (n : ℝ) + 1 := by exact_mod_cast h1
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 121 at 612c41e635db ↗
  hrat.hbound.h4 have (0 : ℝ) ≤ ((2 : ℝ) ^ n)⁻¹ routine: positivity
  Leaves (↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n ≤ (↑n : ℝ) ^ (1 : ℕ) * (1 / 2 : ℝ) ^ n + (1 / 2 : ℝ) ^ n, with h4 : (0 : ℝ) ≤ ((2 : ℝ) ^ n)⁻¹.
  Lean, line 122
  have h4 : (0 : ℝ) ≤ ((2 : ℝ) ^ n)⁻¹ := by positivity
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 122 at 612c41e635db ↗
3. hrat.hsum have Summable fun (n : ℕ) => (↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n
  Leaves ∃ (t : ℤ), (↑q : ℝ) * (∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (m + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) + ∑ p ∈ a.primeFactors, ∑' (k : ℕ), (if p ∣ m + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ))) = (↑t : ℝ), with hsum : Summable fun (n : ℕ) => (↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n.
  Uses library Summable, Summable.of_nonneg_of_le, summable_pow_mul_geometric_of_norm_lt_one, Real.norm_eq_abs, summable_geometric_of_lt_one.
  Lean, lines 125–128
  have hsum : Summable (fun n : ℕ => (ω n : ℝ) / 2 ^ n) := by refine Summable.of_nonneg_of_le (fun n => by positivity) hbound ?_ exact (summable_pow_mul_geometric_of_norm_lt_one 1 (by norm_num [Real.norm_eq_abs])).add (summable_geometric_of_lt_one (by norm_num) (by norm_num))
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 125–128 at 612c41e635db ↗
4. hrat.htail have ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (m + (k + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) = (2 : ℝ) ^ m * (∑' (n : ℕ), (↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n - ∑ n ∈ Finset.range (m + (1 : ℕ)), (↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n)
  Leaves ∃ (t : ℤ), (↑q : ℝ) * (∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (m + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) + ∑ p ∈ a.primeFactors, ∑' (k : ℕ), (if p ∣ m + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ))) = (↑t : ℝ), with htail : ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (m + (k + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) = (2 : ℝ) ^ m * (∑' (n : ℕ), (↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n - ∑ n ∈ Finset.range (m + (1 : ℕ)), (↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n).
  Uses library Finset.range.
  Lean, lines 129–142
  have htail : ∑' k : ℕ, (ω (m + (k + 1)) : ℝ) / 2 ^ (k + 1) = 2 ^ m * (∑' n : ℕ, (ω n : ℝ) / 2 ^ n - ∑ n ∈ Finset.range (m + 1), (ω n : ℝ) / 2 ^ n) := by have h := hsum.sum_add_tsum_nat_add (m + 1) have h2 : ∑' i : ℕ, (ω (i + (m + 1)) : ℝ) / 2 ^ (i + (m + 1)) = (∑' k : ℕ, (ω (m + (k + 1)) : ℝ) / 2 ^ (k + 1)) / 2 ^ m := by rw [← tsum_div_const] refine tsum_congr (fun k => ?_) rw [show k + (m + 1) = m + (k + 1) by ring, show m + (k + 1) = (k + 1) + m by ring, pow_add, div_div] rw [h2] at h have h3 := eq_sub_of_add_eq' h rw [← h3] field_simp
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 129–142 at 612c41e635db ↗
  hrat.htail.h have ∑ i ∈ Finset.range (m + (1 : ℕ)), (↑((ω : ℕ → ℕ) i) : ℝ) / (2 : ℝ) ^ i + ∑' (i : ℕ), (↑((ω : ℕ → ℕ) (i + (m + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (i + (m + (1 : ℕ))) = ∑' (i : ℕ), (↑((ω : ℕ → ℕ) i) : ℝ) / (2 : ℝ) ^ i
  Leaves ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (m + (k + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) = (2 : ℝ) ^ m * (∑' (n : ℕ), (↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n - ∑ n ∈ Finset.range (m + (1 : ℕ)), (↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n), with h : ∑ i ∈ Finset.range (m + (1 : ℕ)), (↑((ω : ℕ → ℕ) i) : ℝ) / (2 : ℝ) ^ i + ∑' (i : ℕ), (↑((ω : ℕ → ℕ) (i + (m + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (i + (m + (1 : ℕ))) = ∑' (i : ℕ), (↑((ω : ℕ → ℕ) i) : ℝ) / (2 : ℝ) ^ i.
  Lean, line 132
  have h := hsum.sum_add_tsum_nat_add (m + 1)
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 132 at 612c41e635db ↗
  hrat.htail.h2 have ∑' (i : ℕ), (↑((ω : ℕ → ℕ) (i + (m + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (i + (m + (1 : ℕ))) = (∑' (k : ℕ), (↑((ω : ℕ → ℕ) (m + (k + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ))) / (2 : ℝ) ^ m
  Leaves ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (m + (k + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) = (2 : ℝ) ^ m * (∑' (n : ℕ), (↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n - ∑ n ∈ Finset.range (m + (1 : ℕ)), (↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n), with h2 : ∑' (i : ℕ), (↑((ω : ℕ → ℕ) (i + (m + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (i + (m + (1 : ℕ))) = (∑' (k : ℕ), (↑((ω : ℕ → ℕ) (m + (k + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ))) / (2 : ℝ) ^ m.
  Uses library tsum_div_const, tsum_congr, pow_add, div_div.
  Lean, lines 133–138
  have h2 : ∑' i : ℕ, (ω (i + (m + 1)) : ℝ) / 2 ^ (i + (m + 1)) = (∑' k : ℕ, (ω (m + (k + 1)) : ℝ) / 2 ^ (k + 1)) / 2 ^ m := by rw [← tsum_div_const] refine tsum_congr (fun k => ?_) rw [show k + (m + 1) = m + (k + 1) by ring, show m + (k + 1) = (k + 1) + m by ring, pow_add, div_div]
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 133–138 at 612c41e635db ↗
  hrat.htail.h3 have (∑' (k : ℕ), (↑((ω : ℕ → ℕ) (m + (k + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ))) / (2 : ℝ) ^ m = ∑' (i : ℕ), (↑((ω : ℕ → ℕ) i) : ℝ) / (2 : ℝ) ^ i - ∑ i ∈ Finset.range (m + (1 : ℕ)), (↑((ω : ℕ → ℕ) i) : ℝ) / (2 : ℝ) ^ i
  Leaves ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (m + (k + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) = (2 : ℝ) ^ m * (∑' (n : ℕ), (↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n - ∑ n ∈ Finset.range (m + (1 : ℕ)), (↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n), with h3 : (∑' (k : ℕ), (↑((ω : ℕ → ℕ) (m + (k + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ))) / (2 : ℝ) ^ m = ∑' (i : ℕ), (↑((ω : ℕ → ℕ) i) : ℝ) / (2 : ℝ) ^ i - ∑ i ∈ Finset.range (m + (1 : ℕ)), (↑((ω : ℕ → ℕ) i) : ℝ) / (2 : ℝ) ^ i.
  Uses library eq_sub_of_add_eq'.
  Lean, line 140
  have h3 := eq_sub_of_add_eq' h
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 140 at 612c41e635db ↗
5. hrat.hA have ∑ n ∈ Finset.range (m + (1 : ℕ)), (↑q : ℝ) * (↑((ω : ℕ → ℕ) n) : ℝ) * (2 : ℝ) ^ (m - n) = (2 : ℝ) ^ m * ((↑q : ℝ) * ∑ n ∈ Finset.range (m + (1 : ℕ)), (↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n)
  Leaves ∃ (t : ℤ), (↑q : ℝ) * (∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (m + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) + ∑ p ∈ a.primeFactors, ∑' (k : ℕ), (if p ∣ m + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ))) = (↑t : ℝ), with hA : ∑ n ∈ Finset.range (m + (1 : ℕ)), (↑q : ℝ) * (↑((ω : ℕ → ℕ) n) : ℝ) * (2 : ℝ) ^ (m - n) = (2 : ℝ) ^ m * ((↑q : ℝ) * ∑ n ∈ Finset.range (m + (1 : ℕ)), (↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n).
  Uses library Finset.range, Finset.mul_sum, Finset.sum_congr, rfl, pow_sub₀, two_ne_zero.
  Lean, lines 143–149
  have hA : ∑ n ∈ Finset.range (m + 1), (q : ℝ) * (ω n : ℝ) * 2 ^ (m - n) = 2 ^ m * ((q : ℝ) * ∑ n ∈ Finset.range (m + 1), (ω n : ℝ) / 2 ^ n) := by rw [Finset.mul_sum, Finset.mul_sum] refine Finset.sum_congr rfl (fun n hn => ?_) have hn' : n ≤ m := Nat.lt_succ_iff.1 (Finset.mem_range.1 hn) rw [pow_sub₀ (2 : ℝ) two_ne_zero hn'] field_simp
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 143–149 at 612c41e635db ↗
  hrat.hA.hn' have n ≤ m
  Leaves (↑q : ℝ) * (↑((ω : ℕ → ℕ) n) : ℝ) * (2 : ℝ) ^ (m - n) = (2 : ℝ) ^ m * ((↑q : ℝ) * ((↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n)), with hn' : n ≤ m.
  Uses library Nat.lt_succ_iff, Finset.mem_range.
  Lean, line 147
  have hn' : n ≤ m := Nat.lt_succ_iff.1 (Finset.mem_range.1 hn)
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 147 at 612c41e635db ↗
hmean have (∑ t ∈ Finset.range T, ∑ p ∈ a.primeFactors, ∑' (k : ℕ), (if p ∣ b + Q * t + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ))) / (↑T : ℝ) ≤ ∑ p ∈ a.primeFactors, ((1 : ℝ) / (↑p : ℝ) + (1 : ℝ) / (↑T : ℝ))
Leaves (∑ t ∈ Finset.range T, |(↑q : ℝ) * ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (b + Q * t + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) - (↑(round ((↑q : ℝ) * ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (b + Q * t + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)))) : ℝ)|) / (↑T : ℝ) ≤ (↑q : ℝ) * ∑ p ∈ a.primeFactors, ((1 : ℝ) / (↑p : ℝ) + (1 : ℝ) / (↑T : ℝ)), with hmean : (∑ t ∈ Finset.range T, ∑ p ∈ a.primeFactors, ∑' (k : ℕ), (if p ∣ b + Q * t + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ))) / (↑T : ℝ) ≤ ∑ p ∈ a.primeFactors, ((1 : ℝ) / (↑p : ℝ) + (1 : ℝ) / (↑T : ℝ)).
Uses library Finset.range, div_le_iff₀, Finset.sum_comm, Finset.sum_mul, Finset.sum_le_sum.
Lean, lines 155–266
```
  have hmean : (∑ t ∈ Finset.range T, ∑ p ∈ a.primeFactors,
          ∑' k : ℕ, (if p ∣ b + Q * t + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1)) / T
        ≤ ∑ p ∈ a.primeFactors, ((1 : ℝ) / p + 1 / T) := by
    have hcount : ∀ (p Q c T : ℕ), p.Prime → Nat.Coprime p Q →
        ((Finset.range T).filter (fun t => p ∣ c + Q * t)).card ≤ T / p + 1 := by
      intro p Q c T hp hQ
      have hp0 : 0 < p := hp.pos
      have key := Finset.card_le_card_of_injOn (s := (Finset.range T).filter (fun t => p ∣ c + Q * t))
        (t := Finset.range (T / p + 1)) (fun t => t / p) ?_ ?_
      · simpa using key
      · intro t ht
        have ht1 : t < T := (Finset.mem_range.1 (Finset.mem_filter.1 ht).1)
        exact Finset.mem_coe.2 (Finset.mem_range.2 (Nat.lt_succ_of_le (Nat.div_le_div_right ht1.le)))
      · intro t ht t' ht' heq
        have ht := Finset.mem_filter.1 (Finset.mem_coe.1 ht)
        have ht' := Finset.mem_filter.1 (Finset.mem_coe.1 ht')
        rw [Finset.mem_range] at ht ht'
        have heq' : t / p = t' / p := heq
        -- p ∣ Q * (t - t') in ℤ
        have hz : (p : ℤ) ∣ (Q : ℤ) * ((t : ℤ) - t') := by
          have h1 : (p : ℤ) ∣ (c : ℤ) + Q * t := by exact_mod_cast ht.2
          have h2 : (p : ℤ) ∣ (c : ℤ) + Q * t' := by exact_mod_cast ht'.2
          have := dvd_sub h1 h2
          have e : (c : ℤ) + Q * t - (c + Q * t') = Q * (t - t') := by ring
          rwa [e] at this
        have hpQ : ¬ (p : ℤ) ∣ Q := by
          intro h
          have : p ∣ Q := by exact_mod_cast h
          have := Nat.Coprime.eq_one_of_dvd hQ this
          exact hp.one_lt.ne' this
        have hpd : (p : ℤ) ∣ (t : ℤ) - t' :=
          (Int.Prime.dvd_mul' hp hz).resolve_left hpQ
        -- |t - t'| < p
        have hlt1 : (t : ℤ) - t' < p := by
          have a1 := Nat.div_add_mod t p
          have a2 := Nat.div_add_mod t' p
          have b1 := Nat.mod_lt t hp0
          have b2 := Nat.mod_lt t' hp0
          rw [heq'] at a1
          omega
        have hlt2 : (t' : ℤ) - t < p := by
          have a1 := Nat.div_add_mod t p
          have a2 := Nat.div_add_mod t' p
          have b1 := Nat.mod_lt t hp0
          have b2 := Nat.mod_lt t' hp0
          rw [heq'] at a1
          omega
        obtain ⟨k, hk⟩ := hpd
        have hp' : (0 : ℤ) < p := by exact_mod_cast hp0
        have : k = 0 := by
          rcases lt_trichotomy k 0 with h | h | h
          · nlinarith
          · exact h
          · nlinarith
        rw [this, mul_zero] at hk
        omega
    have hTpos : (0 : ℝ) < T := by exact_mod_cast hT
    have hS2 : Summable (fun k : ℕ => (1 : ℝ) / 2 ^ (k + 1)) := by
      refine Summable.of_nonneg_of_le (fun k => by positivity) (fun k => ?_)
        (summable_geometric_of_lt_one (by norm_num : (0 : ℝ) ≤ 1 / 2) (by norm_num))
      rw [one_div_pow, pow_succ]
      apply one_div_le_one_div_of_le (by positivity)
      linarith [pow_pos (by norm_num : (0 : ℝ) < 2) k]
    have hsum1 : ∑' k : ℕ, (1 : ℝ) / 2 ^ (k + 1) = 1 := by
      have : (fun k : ℕ => (1 : ℝ) / 2 ^ (k + 1)) = fun k => (1 / 2) * (1 / 2 : ℝ) ^ k := by
        funext k; rw [pow_succ, one_div_pow]; field_simp
      rw [this, tsum_mul_left, tsum_geometric_two]; norm_num
    have hind : ∀ (p t : ℕ), Summable (fun k : ℕ =>
        (if p ∣ b + Q * t + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1)) := by
      intro p t
      refine Summable.of_nonneg_of_le (fun k => by split_ifs <;> positivity) (fun k => ?_) hS2
      split_ifs <;> simp
    -- one prime at a time
    have hper : ∀ p ∈ a.primeFactors, ∑ t ∈ Finset.range T,
        ∑' k : ℕ, (if p ∣ b + Q * t + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1)
          ≤ (T : ℝ) / p + 1 := by
      intro p hp
      have hpp : p.Prime := Nat.prime_of_mem_primeFactors hp
      have hppos : (0 : ℝ) < p := by exact_mod_cast hpp.pos
      rw [← Summable.tsum_finsetSum (fun t _ => hind p t)]
      have hk : ∀ k : ℕ, ∑ t ∈ Finset.range T,
          (if p ∣ b + Q * t + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1)
            ≤ ((T : ℝ) / p + 1) * (1 / 2 ^ (k + 1)) := by
        intro k
        rw [← Finset.sum_div, Finset.sum_boole]
        have hc := hcount p Q (b + (k + 1)) T hpp (hcop p hp)
        have hfe : (Finset.range T).filter (fun t => p ∣ b + Q * t + (k + 1))
            = (Finset.range T).filter (fun t => p ∣ b + (k + 1) + Q * t) := by
          apply Finset.filter_congr
          intro t _
          rw [show b + Q * t + (k + 1) = b + (k + 1) + Q * t by ring]
        rw [hfe]
        have hc' : (((Finset.range T).filter (fun t => p ∣ b + (k + 1) + Q * t)).card : ℝ)
            ≤ (T : ℝ) / p + 1 := by
          have h1 : ((T / p : ℕ) : ℝ) ≤ (T : ℝ) / p := Nat.cast_div_le
          have h2 : (((Finset.range T).filter (fun t => p ∣ b + (k + 1) + Q * t)).card : ℝ)
              ≤ ((T / p : ℕ) : ℝ) + 1 := by exact_mod_cast hc
          linarith
        rw [div_eq_mul_one_div]
        exact mul_le_mul_of_nonneg_right hc' (by positivity)
      calc ∑' k : ℕ, ∑ t ∈ Finset.range T,
            (if p ∣ b + Q * t + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1)
          ≤ ∑' k : ℕ, ((T : ℝ) / p + 1) * (1 / 2 ^ (k + 1)) :=
            Summable.tsum_le_tsum hk (summable_sum (fun t _ => hind p t)) (hS2.mul_left _)
        _ = (T : ℝ) / p + 1 := by rw [tsum_mul_left, hsum1, mul_one]
    rw [div_le_iff₀ hTpos, Finset.sum_comm, Finset.sum_mul]
    refine Finset.sum_le_sum (fun p hp => ?_)
    have hppos : (0 : ℝ) < p := by exact_mod_cast (Nat.prime_of_mem_primeFactors hp).pos
    calc ∑ t ∈ Finset.range T,
          ∑' k : ℕ, (if p ∣ b + Q * t + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1)
        ≤ (T : ℝ) / p + 1 := hper p hp
      _ = ((1 : ℝ) / p + 1 / T) * T := by field_simp
```
targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 155–266 at 612c41e635db ↗
1. hmean.hcount have ∀ (p Q c T : ℕ), Nat.Prime p → p.Coprime Q → {t ∈ Finset.range T | p ∣ c + Q * t}.card ≤ T / p + (1 : ℕ)
  Leaves (∑ t ∈ Finset.range T, ∑ p ∈ a.primeFactors, ∑' (k : ℕ), (if p ∣ b + Q * t + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ))) / (↑T : ℝ) ≤ ∑ p ∈ a.primeFactors, ((1 : ℝ) / (↑p : ℝ) + (1 : ℝ) / (↑T : ℝ)), with hcount : ∀ (p Q c T : ℕ), Nat.Prime p → p.Coprime Q → {t ∈ Finset.range T | p ∣ c + Q * t}.card ≤ T / p + (1 : ℕ).
  Uses library Nat.Coprime, Finset.range.
  Lean, lines 158–210
  have hcount : ∀ (p Q c T : ℕ), p.Prime → Nat.Coprime p Q → ((Finset.range T).filter (fun t => p ∣ c + Q * t)).card ≤ T / p + 1 := by intro p Q c T hp hQ have hp0 : 0 < p := hp.pos have key := Finset.card_le_card_of_injOn (s := (Finset.range T).filter (fun t => p ∣ c + Q * t)) (t := Finset.range (T / p + 1)) (fun t => t / p) ?_ ?_ · simpa using key · intro t ht have ht1 : t < T := (Finset.mem_range.1 (Finset.mem_filter.1 ht).1) exact Finset.mem_coe.2 (Finset.mem_range.2 (Nat.lt_succ_of_le (Nat.div_le_div_right ht1.le))) · intro t ht t' ht' heq have ht := Finset.mem_filter.1 (Finset.mem_coe.1 ht) have ht' := Finset.mem_filter.1 (Finset.mem_coe.1 ht') rw [Finset.mem_range] at ht ht' have heq' : t / p = t' / p := heq -- p ∣ Q * (t - t') in ℤ have hz : (p : ℤ) ∣ (Q : ℤ) * ((t : ℤ) - t') := by have h1 : (p : ℤ) ∣ (c : ℤ) + Q * t := by exact_mod_cast ht.2 have h2 : (p : ℤ) ∣ (c : ℤ) + Q * t' := by exact_mod_cast ht'.2 have := dvd_sub h1 h2 have e : (c : ℤ) + Q * t - (c + Q * t') = Q * (t - t') := by ring rwa [e] at this have hpQ : ¬ (p : ℤ) ∣ Q := by intro h have : p ∣ Q := by exact_mod_cast h have := Nat.Coprime.eq_one_of_dvd hQ this exact hp.one_lt.ne' this have hpd : (p : ℤ) ∣ (t : ℤ) - t' := (Int.Prime.dvd_mul' hp hz).resolve_left hpQ -- |t - t'| < p have hlt1 : (t : ℤ) - t' < p := by have a1 := Nat.div_add_mod t p have a2 := Nat.div_add_mod t' p have b1 := Nat.mod_lt t hp0 have b2 := Nat.mod_lt t' hp0 rw [heq'] at a1 omega have hlt2 : (t' : ℤ) - t < p := by have a1 := Nat.div_add_mod t p have a2 := Nat.div_add_mod t' p have b1 := Nat.mod_lt t hp0 have b2 := Nat.mod_lt t' hp0 rw [heq'] at a1 omega obtain ⟨k, hk⟩ := hpd have hp' : (0 : ℤ) < p := by exact_mod_cast hp0 have : k = 0 := by rcases lt_trichotomy k 0 with h | h | h · nlinarith · exact h · nlinarith rw [this, mul_zero] at hk omega
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 158–210 at 612c41e635db ↗
  hmean.hcount.hp0 have (0 : ℕ) < p
  Leaves {t ∈ Finset.range T | p ∣ c + Q * t}.card ≤ T / p + (1 : ℕ), with hp0 : (0 : ℕ) < p.
  Lean, line 161
  have hp0 : 0 < p := hp.pos
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 161 at 612c41e635db ↗
  hmean.hcount.key have {t ∈ Finset.range T | p ∣ c + Q * t}.card ≤ (Finset.range (T / p + (1 : ℕ))).card
  Leaves {t ∈ Finset.range T | p ∣ c + Q * t}.card ≤ T / p + (1 : ℕ), with key : {t ∈ Finset.range T | p ∣ c + Q * t}.card ≤ (Finset.range (T / p + (1 : ℕ))).card.
  Uses library Finset.card_le_card_of_injOn, Finset.range.
  Lean, lines 162–163
  have key := Finset.card_le_card_of_injOn (s := (Finset.range T).filter (fun t => p ∣ c + Q * t)) (t := Finset.range (T / p + 1)) (fun t => t / p) ?_ ?_
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 162–163 at 612c41e635db ↗
  hmean.hcount.s3 case
  Leaves {t ∈ Finset.range T | p ∣ c + Q * t}.card ≤ T / p + (1 : ℕ).
  Lean, line 164
  · simpa using key
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 164 at 612c41e635db ↗
  hmean.hcount.s4 case
  Leaves Set.MapsTo (fun (t : ℕ) => t / p) (↑({t ∈ Finset.range T | p ∣ c + Q * t}) : Set ℕ) (↑(Finset.range (T / p + (1 : ℕ))) : Set ℕ).
  Uses library Finset.mem_coe, Finset.mem_range, Nat.lt_succ_of_le, Nat.div_le_div_right.
  Lean, lines 165–167
  · intro t ht have ht1 : t < T := (Finset.mem_range.1 (Finset.mem_filter.1 ht).1) exact Finset.mem_coe.2 (Finset.mem_range.2 (Nat.lt_succ_of_le (Nat.div_le_div_right ht1.le)))
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 165–167 at 612c41e635db ↗
  hmean.hcount.s4.ht1 have t < T
  Leaves (fun (t : ℕ) => t / p) t ∈ (↑(Finset.range (T / p + (1 : ℕ))) : Set ℕ), with ht1 : t < T.
  Uses library Finset.mem_range, Finset.mem_filter.
  Lean, line 166
  have ht1 : t < T := (Finset.mem_range.1 (Finset.mem_filter.1 ht).1)
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 166 at 612c41e635db ↗
  hmean.hcount.s5 case
  Leaves Set.InjOn (fun (t : ℕ) => t / p) (↑({t ∈ Finset.range T | p ∣ c + Q * t}) : Set ℕ).
  Uses library Finset.mem_range, MulZeroClass.mul_zero.
  Lean, lines 168–210
  · intro t ht t' ht' heq have ht := Finset.mem_filter.1 (Finset.mem_coe.1 ht) have ht' := Finset.mem_filter.1 (Finset.mem_coe.1 ht') rw [Finset.mem_range] at ht ht' have heq' : t / p = t' / p := heq -- p ∣ Q * (t - t') in ℤ have hz : (p : ℤ) ∣ (Q : ℤ) * ((t : ℤ) - t') := by have h1 : (p : ℤ) ∣ (c : ℤ) + Q * t := by exact_mod_cast ht.2 have h2 : (p : ℤ) ∣ (c : ℤ) + Q * t' := by exact_mod_cast ht'.2 have := dvd_sub h1 h2 have e : (c : ℤ) + Q * t - (c + Q * t') = Q * (t - t') := by ring rwa [e] at this have hpQ : ¬ (p : ℤ) ∣ Q := by intro h have : p ∣ Q := by exact_mod_cast h have := Nat.Coprime.eq_one_of_dvd hQ this exact hp.one_lt.ne' this have hpd : (p : ℤ) ∣ (t : ℤ) - t' := (Int.Prime.dvd_mul' hp hz).resolve_left hpQ -- |t - t'| < p have hlt1 : (t : ℤ) - t' < p := by have a1 := Nat.div_add_mod t p have a2 := Nat.div_add_mod t' p have b1 := Nat.mod_lt t hp0 have b2 := Nat.mod_lt t' hp0 rw [heq'] at a1 omega have hlt2 : (t' : ℤ) - t < p := by have a1 := Nat.div_add_mod t p have a2 := Nat.div_add_mod t' p have b1 := Nat.mod_lt t hp0 have b2 := Nat.mod_lt t' hp0 rw [heq'] at a1 omega obtain ⟨k, hk⟩ := hpd have hp' : (0 : ℤ) < p := by exact_mod_cast hp0 have : k = 0 := by rcases lt_trichotomy k 0 with h | h | h · nlinarith · exact h · nlinarith rw [this, mul_zero] at hk omega
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 168–210 at 612c41e635db ↗
  hmean.hcount.s5.ht have t ∈ Finset.range T ∧ p ∣ c + Q * t
  Leaves t = t', with ht : t ∈ Finset.range T ∧ p ∣ c + Q * t.
  Uses library Finset.mem_filter, Finset.mem_coe.
  Lean, line 169
  have ht := Finset.mem_filter.1 (Finset.mem_coe.1 ht)
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 169 at 612c41e635db ↗
  hmean.hcount.s5.ht' have t' ∈ Finset.range T ∧ p ∣ c + Q * t'
  Leaves t = t', with ht' : t' ∈ Finset.range T ∧ p ∣ c + Q * t'.
  Uses library Finset.mem_filter, Finset.mem_coe.
  Lean, line 170
  have ht' := Finset.mem_filter.1 (Finset.mem_coe.1 ht')
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 170 at 612c41e635db ↗
  hmean.hcount.s5.heq' have t / p = t' / p
  Leaves t = t', with heq' : t / p = t' / p.
  Lean, line 172
  have heq' : t / p = t' / p := heq
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 172 at 612c41e635db ↗
  hmean.hcount.s5.hz have (↑p : ℤ) ∣ (↑Q : ℤ) * ((↑t : ℤ) - (↑t' : ℤ))
  Leaves t = t', with hz : (↑p : ℤ) ∣ (↑Q : ℤ) * ((↑t : ℤ) - (↑t' : ℤ)).
  Lean, lines 174–179
  have hz : (p : ℤ) ∣ (Q : ℤ) * ((t : ℤ) - t') := by have h1 : (p : ℤ) ∣ (c : ℤ) + Q * t := by exact_mod_cast ht.2 have h2 : (p : ℤ) ∣ (c : ℤ) + Q * t' := by exact_mod_cast ht'.2 have := dvd_sub h1 h2 have e : (c : ℤ) + Q * t - (c + Q * t') = Q * (t - t') := by ring rwa [e] at this
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 174–179 at 612c41e635db ↗
  hmean.hcount.s5.hz.h1 have (↑p : ℤ) ∣ (↑c : ℤ) + (↑Q : ℤ) * (↑t : ℤ)
  Leaves (↑p : ℤ) ∣ (↑Q : ℤ) * ((↑t : ℤ) - (↑t' : ℤ)), with h1 : (↑p : ℤ) ∣ (↑c : ℤ) + (↑Q : ℤ) * (↑t : ℤ).
  Lean, line 175
  have h1 : (p : ℤ) ∣ (c : ℤ) + Q * t := by exact_mod_cast ht.2
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 175 at 612c41e635db ↗
  hmean.hcount.s5.hz.h2 have (↑p : ℤ) ∣ (↑c : ℤ) + (↑Q : ℤ) * (↑t' : ℤ)
  Leaves (↑p : ℤ) ∣ (↑Q : ℤ) * ((↑t : ℤ) - (↑t' : ℤ)), with h2 : (↑p : ℤ) ∣ (↑c : ℤ) + (↑Q : ℤ) * (↑t' : ℤ).
  Lean, line 176
  have h2 : (p : ℤ) ∣ (c : ℤ) + Q * t' := by exact_mod_cast ht'.2
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 176 at 612c41e635db ↗
  hmean.hcount.s5.hz.this have (↑p : ℤ) ∣ (↑c : ℤ) + (↑Q : ℤ) * (↑t : ℤ) - ((↑c : ℤ) + (↑Q : ℤ) * (↑t' : ℤ))
  Leaves (↑p : ℤ) ∣ (↑Q : ℤ) * ((↑t : ℤ) - (↑t' : ℤ)), with this : (↑p : ℤ) ∣ (↑c : ℤ) + (↑Q : ℤ) * (↑t : ℤ) - ((↑c : ℤ) + (↑Q : ℤ) * (↑t' : ℤ)).
  Uses library dvd_sub.
  Lean, line 177
  have := dvd_sub h1 h2
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 177 at 612c41e635db ↗
  hmean.hcount.s5.hz.e have (↑c : ℤ) + (↑Q : ℤ) * (↑t : ℤ) - ((↑c : ℤ) + (↑Q : ℤ) * (↑t' : ℤ)) = (↑Q : ℤ) * ((↑t : ℤ) - (↑t' : ℤ)) routine: ring
  Leaves (↑p : ℤ) ∣ (↑Q : ℤ) * ((↑t : ℤ) - (↑t' : ℤ)), with e : (↑c : ℤ) + (↑Q : ℤ) * (↑t : ℤ) - ((↑c : ℤ) + (↑Q : ℤ) * (↑t' : ℤ)) = (↑Q : ℤ) * ((↑t : ℤ) - (↑t' : ℤ)).
  Lean, line 178
  have e : (c : ℤ) + Q * t - (c + Q * t') = Q * (t - t') := by ring
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 178 at 612c41e635db ↗
  hmean.hcount.s5.hpQ have ¬(↑p : ℤ) ∣ (↑Q : ℤ)
  Leaves t = t', with hpQ : ¬(↑p : ℤ) ∣ (↑Q : ℤ).
  Lean, lines 180–184
  have hpQ : ¬ (p : ℤ) ∣ Q := by intro h have : p ∣ Q := by exact_mod_cast h have := Nat.Coprime.eq_one_of_dvd hQ this exact hp.one_lt.ne' this
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 180–184 at 612c41e635db ↗
  hmean.hcount.s5.hpQ.s1 have p ∣ Q
  Leaves False, with this : p ∣ Q.
  Lean, line 182
  have : p ∣ Q := by exact_mod_cast h
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 182 at 612c41e635db ↗
  hmean.hcount.s5.hpQ.s2 have p = (1 : ℕ)
  Leaves False, with this : p = (1 : ℕ).
  Uses library Nat.Coprime.eq_one_of_dvd.
  Lean, line 183
  have := Nat.Coprime.eq_one_of_dvd hQ this
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 183 at 612c41e635db ↗
  hmean.hcount.s5.hpd have (↑p : ℤ) ∣ (↑t : ℤ) - (↑t' : ℤ)
  Leaves t = t', with hpd : (↑p : ℤ) ∣ (↑t : ℤ) - (↑t' : ℤ).
  Uses library Int.Prime.dvd_mul'.
  Lean, lines 185–186
  have hpd : (p : ℤ) ∣ (t : ℤ) - t' := (Int.Prime.dvd_mul' hp hz).resolve_left hpQ
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 185–186 at 612c41e635db ↗
  hmean.hcount.s5.hlt1 have (↑t : ℤ) - (↑t' : ℤ) < (↑p : ℤ)
  Leaves t = t', with hlt1 : (↑t : ℤ) - (↑t' : ℤ) < (↑p : ℤ).
  Lean, lines 188–194
  have hlt1 : (t : ℤ) - t' < p := by have a1 := Nat.div_add_mod t p have a2 := Nat.div_add_mod t' p have b1 := Nat.mod_lt t hp0 have b2 := Nat.mod_lt t' hp0 rw [heq'] at a1 omega
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 188–194 at 612c41e635db ↗
  hmean.hcount.s5.hlt1.a1 have p * (t / p) + t % p = t
  Leaves (↑t : ℤ) - (↑t' : ℤ) < (↑p : ℤ), with a1 : p * (t / p) + t % p = t.
  Uses library Nat.div_add_mod.
  Lean, line 189
  have a1 := Nat.div_add_mod t p
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 189 at 612c41e635db ↗
  hmean.hcount.s5.hlt1.a2 have p * (t' / p) + t' % p = t'
  Leaves (↑t : ℤ) - (↑t' : ℤ) < (↑p : ℤ), with a2 : p * (t' / p) + t' % p = t'.
  Uses library Nat.div_add_mod.
  Lean, line 190
  have a2 := Nat.div_add_mod t' p
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 190 at 612c41e635db ↗
  hmean.hcount.s5.hlt1.b1 have t % p < p
  Leaves (↑t : ℤ) - (↑t' : ℤ) < (↑p : ℤ), with b1 : t % p < p.
  Uses library Nat.mod_lt.
  Lean, line 191
  have b1 := Nat.mod_lt t hp0
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 191 at 612c41e635db ↗
  hmean.hcount.s5.hlt1.b2 have t' % p < p
  Leaves (↑t : ℤ) - (↑t' : ℤ) < (↑p : ℤ), with b2 : t' % p < p.
  Uses library Nat.mod_lt.
  Lean, line 192
  have b2 := Nat.mod_lt t' hp0
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 192 at 612c41e635db ↗
  hmean.hcount.s5.hlt2 have (↑t' : ℤ) - (↑t : ℤ) < (↑p : ℤ)
  Leaves t = t', with hlt2 : (↑t' : ℤ) - (↑t : ℤ) < (↑p : ℤ).
  Lean, lines 195–201
  have hlt2 : (t' : ℤ) - t < p := by have a1 := Nat.div_add_mod t p have a2 := Nat.div_add_mod t' p have b1 := Nat.mod_lt t hp0 have b2 := Nat.mod_lt t' hp0 rw [heq'] at a1 omega
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 195–201 at 612c41e635db ↗
  hmean.hcount.s5.hlt2.a1 have p * (t / p) + t % p = t
  Leaves (↑t' : ℤ) - (↑t : ℤ) < (↑p : ℤ), with a1 : p * (t / p) + t % p = t.
  Uses library Nat.div_add_mod.
  Lean, line 196
  have a1 := Nat.div_add_mod t p
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 196 at 612c41e635db ↗
  hmean.hcount.s5.hlt2.a2 have p * (t' / p) + t' % p = t'
  Leaves (↑t' : ℤ) - (↑t : ℤ) < (↑p : ℤ), with a2 : p * (t' / p) + t' % p = t'.
  Uses library Nat.div_add_mod.
  Lean, line 197
  have a2 := Nat.div_add_mod t' p
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 197 at 612c41e635db ↗
  hmean.hcount.s5.hlt2.b1 have t % p < p
  Leaves (↑t' : ℤ) - (↑t : ℤ) < (↑p : ℤ), with b1 : t % p < p.
  Uses library Nat.mod_lt.
  Lean, line 198
  have b1 := Nat.mod_lt t hp0
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 198 at 612c41e635db ↗
  hmean.hcount.s5.hlt2.b2 have t' % p < p
  Leaves (↑t' : ℤ) - (↑t : ℤ) < (↑p : ℤ), with b2 : t' % p < p.
  Uses library Nat.mod_lt.
  Lean, line 199
  have b2 := Nat.mod_lt t' hp0
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 199 at 612c41e635db ↗
  hmean.hcount.s5.s9 obtain (↑p : ℤ) ∣ (↑t : ℤ) - (↑t' : ℤ)
  Leaves t = t', with k : ℤ, hk : (↑t : ℤ) - (↑t' : ℤ) = (↑p : ℤ) * k.
  Lean, line 202
  obtain ⟨k, hk⟩ := hpd
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 202 at 612c41e635db ↗
  hmean.hcount.s5.hp' have (0 : ℤ) < (↑p : ℤ)
  Leaves t = t', with hp' : (0 : ℤ) < (↑p : ℤ).
  Lean, line 203
  have hp' : (0 : ℤ) < p := by exact_mod_cast hp0
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 203 at 612c41e635db ↗
  hmean.hcount.s5.this have k = (0 : ℤ)
  Leaves t = t', with this : k = (0 : ℤ).
  Uses library lt_trichotomy.
  Lean, lines 204–208
  have : k = 0 := by rcases lt_trichotomy k 0 with h | h | h · nlinarith · exact h · nlinarith
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 204–208 at 612c41e635db ↗
  hmean.hcount.s5.this.s1 case routine: nlinarith
  Leaves k = (0 : ℤ).
  Lean, line 206
  · nlinarith
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 206 at 612c41e635db ↗
  hmean.hcount.s5.this.s2 case
  Leaves k = (0 : ℤ).
  Lean, line 207
  · exact h
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 207 at 612c41e635db ↗
  hmean.hcount.s5.this.s3 case routine: nlinarith
  Leaves k = (0 : ℤ).
  Lean, line 208
  · nlinarith
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 208 at 612c41e635db ↗
2. hmean.hTpos have (0 : ℝ) < (↑T : ℝ)
  Leaves (∑ t ∈ Finset.range T, ∑ p ∈ a.primeFactors, ∑' (k : ℕ), (if p ∣ b + Q * t + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ))) / (↑T : ℝ) ≤ ∑ p ∈ a.primeFactors, ((1 : ℝ) / (↑p : ℝ) + (1 : ℝ) / (↑T : ℝ)), with hTpos : (0 : ℝ) < (↑T : ℝ).
  Lean, line 211
  have hTpos : (0 : ℝ) < T := by exact_mod_cast hT
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 211 at 612c41e635db ↗
3. hmean.hS2 have Summable fun (k : ℕ) => (1 : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ))
  Leaves (∑ t ∈ Finset.range T, ∑ p ∈ a.primeFactors, ∑' (k : ℕ), (if p ∣ b + Q * t + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ))) / (↑T : ℝ) ≤ ∑ p ∈ a.primeFactors, ((1 : ℝ) / (↑p : ℝ) + (1 : ℝ) / (↑T : ℝ)), with hS2 : Summable fun (k : ℕ) => (1 : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)).
  Uses library Summable, Summable.of_nonneg_of_le, summable_geometric_of_lt_one, one_div_pow, pow_succ, one_div_le_one_div_of_le, pow_pos.
  Lean, lines 212–217
  have hS2 : Summable (fun k : ℕ => (1 : ℝ) / 2 ^ (k + 1)) := by refine Summable.of_nonneg_of_le (fun k => by positivity) (fun k => ?_) (summable_geometric_of_lt_one (by norm_num : (0 : ℝ) ≤ 1 / 2) (by norm_num)) rw [one_div_pow, pow_succ] apply one_div_le_one_div_of_le (by positivity) linarith [pow_pos (by norm_num : (0 : ℝ) < 2) k]
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 212–217 at 612c41e635db ↗
4. hmean.hsum1 have ∑' (k : ℕ), (1 : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) = (1 : ℝ)
  Leaves (∑ t ∈ Finset.range T, ∑ p ∈ a.primeFactors, ∑' (k : ℕ), (if p ∣ b + Q * t + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ))) / (↑T : ℝ) ≤ ∑ p ∈ a.primeFactors, ((1 : ℝ) / (↑p : ℝ) + (1 : ℝ) / (↑T : ℝ)), with hsum1 : ∑' (k : ℕ), (1 : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) = (1 : ℝ).
  Uses library tsum_mul_left, tsum_geometric_two.
  Lean, lines 218–221
  have hsum1 : ∑' k : ℕ, (1 : ℝ) / 2 ^ (k + 1) = 1 := by have : (fun k : ℕ => (1 : ℝ) / 2 ^ (k + 1)) = fun k => (1 / 2) * (1 / 2 : ℝ) ^ k := by funext k; rw [pow_succ, one_div_pow]; field_simp rw [this, tsum_mul_left, tsum_geometric_two]; norm_num
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 218–221 at 612c41e635db ↗
  hmean.hsum1.this have (fun (k : ℕ) => (1 : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ))) = fun (k : ℕ) => (1 / 2 : ℝ) * (1 / 2 : ℝ) ^ k
  Leaves ∑' (k : ℕ), (1 : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) = (1 : ℝ), with this : (fun (k : ℕ) => (1 : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ))) = fun (k : ℕ) => (1 / 2 : ℝ) * (1 / 2 : ℝ) ^ k.
  Uses library pow_succ, one_div_pow.
  Lean, lines 219–220
  have : (fun k : ℕ => (1 : ℝ) / 2 ^ (k + 1)) = fun k => (1 / 2) * (1 / 2 : ℝ) ^ k := by funext k; rw [pow_succ, one_div_pow]; field_simp
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 219–220 at 612c41e635db ↗
5. hmean.hind have ∀ (p t : ℕ), Summable fun (k : ℕ) => (if p ∣ b + Q * t + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ))
  Leaves (∑ t ∈ Finset.range T, ∑ p ∈ a.primeFactors, ∑' (k : ℕ), (if p ∣ b + Q * t + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ))) / (↑T : ℝ) ≤ ∑ p ∈ a.primeFactors, ((1 : ℝ) / (↑p : ℝ) + (1 : ℝ) / (↑T : ℝ)), with hind : ∀ (p t : ℕ), Summable fun (k : ℕ) => (if p ∣ b + Q * t + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)).
  Uses library Summable, Summable.of_nonneg_of_le.
  Lean, lines 222–226
  have hind : ∀ (p t : ℕ), Summable (fun k : ℕ => (if p ∣ b + Q * t + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1)) := by intro p t refine Summable.of_nonneg_of_le (fun k => by split_ifs <;> positivity) (fun k => ?_) hS2 split_ifs <;> simp
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 222–226 at 612c41e635db ↗
6. hmean.hper have ∀ p ∈ a.primeFactors, ∑ t ∈ Finset.range T, ∑' (k : ℕ), (if p ∣ b + Q * t + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)) ≤ (↑T : ℝ) / (↑p : ℝ) + (1 : ℝ)
  Leaves (∑ t ∈ Finset.range T, ∑ p ∈ a.primeFactors, ∑' (k : ℕ), (if p ∣ b + Q * t + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ))) / (↑T : ℝ) ≤ ∑ p ∈ a.primeFactors, ((1 : ℝ) / (↑p : ℝ) + (1 : ℝ) / (↑T : ℝ)), with hper : ∀ p ∈ a.primeFactors, ∑ t ∈ Finset.range T, ∑' (k : ℕ), (if p ∣ b + Q * t + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)) ≤ (↑T : ℝ) / (↑p : ℝ) + (1 : ℝ).
  Uses library Finset.range, Summable.tsum_finsetSum.
  Lean, lines 228–259
  have hper : ∀ p ∈ a.primeFactors, ∑ t ∈ Finset.range T, ∑' k : ℕ, (if p ∣ b + Q * t + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1) ≤ (T : ℝ) / p + 1 := by intro p hp have hpp : p.Prime := Nat.prime_of_mem_primeFactors hp have hppos : (0 : ℝ) < p := by exact_mod_cast hpp.pos rw [← Summable.tsum_finsetSum (fun t _ => hind p t)] have hk : ∀ k : ℕ, ∑ t ∈ Finset.range T, (if p ∣ b + Q * t + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1) ≤ ((T : ℝ) / p + 1) * (1 / 2 ^ (k + 1)) := by intro k rw [← Finset.sum_div, Finset.sum_boole] have hc := hcount p Q (b + (k + 1)) T hpp (hcop p hp) have hfe : (Finset.range T).filter (fun t => p ∣ b + Q * t + (k + 1)) = (Finset.range T).filter (fun t => p ∣ b + (k + 1) + Q * t) := by apply Finset.filter_congr intro t _ rw [show b + Q * t + (k + 1) = b + (k + 1) + Q * t by ring] rw [hfe] have hc' : (((Finset.range T).filter (fun t => p ∣ b + (k + 1) + Q * t)).card : ℝ) ≤ (T : ℝ) / p + 1 := by have h1 : ((T / p : ℕ) : ℝ) ≤ (T : ℝ) / p := Nat.cast_div_le have h2 : (((Finset.range T).filter (fun t => p ∣ b + (k + 1) + Q * t)).card : ℝ) ≤ ((T / p : ℕ) : ℝ) + 1 := by exact_mod_cast hc linarith rw [div_eq_mul_one_div] exact mul_le_mul_of_nonneg_right hc' (by positivity) calc ∑' k : ℕ, ∑ t ∈ Finset.range T, (if p ∣ b + Q * t + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1) ≤ ∑' k : ℕ, ((T : ℝ) / p + 1) * (1 / 2 ^ (k + 1)) := Summable.tsum_le_tsum hk (summable_sum (fun t _ => hind p t)) (hS2.mul_left _) _ = (T : ℝ) / p + 1 := by rw [tsum_mul_left, hsum1, mul_one]
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 228–259 at 612c41e635db ↗
  hmean.hper.hpp have Nat.Prime p
  Leaves ∑ t ∈ Finset.range T, ∑' (k : ℕ), (if p ∣ b + Q * t + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)) ≤ (↑T : ℝ) / (↑p : ℝ) + (1 : ℝ), with hpp : Nat.Prime p.
  Uses library Nat.prime_of_mem_primeFactors.
  Lean, line 232
  have hpp : p.Prime := Nat.prime_of_mem_primeFactors hp
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 232 at 612c41e635db ↗
  hmean.hper.hppos have (0 : ℝ) < (↑p : ℝ)
  Leaves ∑ t ∈ Finset.range T, ∑' (k : ℕ), (if p ∣ b + Q * t + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)) ≤ (↑T : ℝ) / (↑p : ℝ) + (1 : ℝ), with hppos : (0 : ℝ) < (↑p : ℝ).
  Lean, line 233
  have hppos : (0 : ℝ) < p := by exact_mod_cast hpp.pos
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 233 at 612c41e635db ↗
  hmean.hper.hk have ∀ (k : ℕ), ∑ t ∈ Finset.range T, (if p ∣ b + Q * t + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)) ≤ ((↑T : ℝ) / (↑p : ℝ) + (1 : ℝ)) * ((1 : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)))
  Leaves ∑' (b_1 : ℕ), ∑ i ∈ Finset.range T, (if p ∣ b + Q * i + (b_1 + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (b_1 + (1 : ℕ)) ≤ (↑T : ℝ) / (↑p : ℝ) + (1 : ℝ), with hk : ∀ (k : ℕ), ∑ t ∈ Finset.range T, (if p ∣ b + Q * t + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)) ≤ ((↑T : ℝ) / (↑p : ℝ) + (1 : ℝ)) * ((1 : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ))).
  Uses library Finset.range, Finset.sum_div, Finset.sum_boole, div_eq_mul_one_div, mul_le_mul_of_nonneg_right.
  Lean, lines 235–254
  have hk : ∀ k : ℕ, ∑ t ∈ Finset.range T, (if p ∣ b + Q * t + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1) ≤ ((T : ℝ) / p + 1) * (1 / 2 ^ (k + 1)) := by intro k rw [← Finset.sum_div, Finset.sum_boole] have hc := hcount p Q (b + (k + 1)) T hpp (hcop p hp) have hfe : (Finset.range T).filter (fun t => p ∣ b + Q * t + (k + 1)) = (Finset.range T).filter (fun t => p ∣ b + (k + 1) + Q * t) := by apply Finset.filter_congr intro t _ rw [show b + Q * t + (k + 1) = b + (k + 1) + Q * t by ring] rw [hfe] have hc' : (((Finset.range T).filter (fun t => p ∣ b + (k + 1) + Q * t)).card : ℝ) ≤ (T : ℝ) / p + 1 := by have h1 : ((T / p : ℕ) : ℝ) ≤ (T : ℝ) / p := Nat.cast_div_le have h2 : (((Finset.range T).filter (fun t => p ∣ b + (k + 1) + Q * t)).card : ℝ) ≤ ((T / p : ℕ) : ℝ) + 1 := by exact_mod_cast hc linarith rw [div_eq_mul_one_div] exact mul_le_mul_of_nonneg_right hc' (by positivity)
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 235–254 at 612c41e635db ↗
  hmean.hper.hk.hc have {t ∈ Finset.range T | p ∣ b + (k + (1 : ℕ)) + Q * t}.card ≤ T / p + (1 : ℕ)
  Leaves (↑{x ∈ Finset.range T | p ∣ b + Q * x + (k + (1 : ℕ))}.card : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) ≤ ((↑T : ℝ) / (↑p : ℝ) + (1 : ℝ)) * ((1 : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ))), with hc : {t ∈ Finset.range T | p ∣ b + (k + (1 : ℕ)) + Q * t}.card ≤ T / p + (1 : ℕ).
  Lean, line 240
  have hc := hcount p Q (b + (k + 1)) T hpp (hcop p hp)
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 240 at 612c41e635db ↗
  hmean.hper.hk.hfe have {t ∈ Finset.range T | p ∣ b + Q * t + (k + (1 : ℕ))} = {t ∈ Finset.range T | p ∣ b + (k + (1 : ℕ)) + Q * t}
  Leaves (↑{x ∈ Finset.range T | p ∣ b + Q * x + (k + (1 : ℕ))}.card : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) ≤ ((↑T : ℝ) / (↑p : ℝ) + (1 : ℝ)) * ((1 : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ))), with hfe : {t ∈ Finset.range T | p ∣ b + Q * t + (k + (1 : ℕ))} = {t ∈ Finset.range T | p ∣ b + (k + (1 : ℕ)) + Q * t}.
  Uses library Finset.range, Finset.filter_congr.
  Lean, lines 241–245
  have hfe : (Finset.range T).filter (fun t => p ∣ b + Q * t + (k + 1)) = (Finset.range T).filter (fun t => p ∣ b + (k + 1) + Q * t) := by apply Finset.filter_congr intro t _ rw [show b + Q * t + (k + 1) = b + (k + 1) + Q * t by ring]
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 241–245 at 612c41e635db ↗
  hmean.hper.hk.hc' have (↑{t ∈ Finset.range T | p ∣ b + (k + (1 : ℕ)) + Q * t}.card : ℝ) ≤ (↑T : ℝ) / (↑p : ℝ) + (1 : ℝ)
  Leaves (↑{t ∈ Finset.range T | p ∣ b + (k + (1 : ℕ)) + Q * t}.card : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) ≤ ((↑T : ℝ) / (↑p : ℝ) + (1 : ℝ)) * ((1 : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ))), with hc' : (↑{t ∈ Finset.range T | p ∣ b + (k + (1 : ℕ)) + Q * t}.card : ℝ) ≤ (↑T : ℝ) / (↑p : ℝ) + (1 : ℝ).
  Uses library Finset.range.
  Lean, lines 247–252
  have hc' : (((Finset.range T).filter (fun t => p ∣ b + (k + 1) + Q * t)).card : ℝ) ≤ (T : ℝ) / p + 1 := by have h1 : ((T / p : ℕ) : ℝ) ≤ (T : ℝ) / p := Nat.cast_div_le have h2 : (((Finset.range T).filter (fun t => p ∣ b + (k + 1) + Q * t)).card : ℝ) ≤ ((T / p : ℕ) : ℝ) + 1 := by exact_mod_cast hc linarith
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 247–252 at 612c41e635db ↗
  hmean.hper.hk.hc'.h1 have (↑(T / p) : ℝ) ≤ (↑T : ℝ) / (↑p : ℝ)
  Leaves (↑{t ∈ Finset.range T | p ∣ b + (k + (1 : ℕ)) + Q * t}.card : ℝ) ≤ (↑T : ℝ) / (↑p : ℝ) + (1 : ℝ), with h1 : (↑(T / p) : ℝ) ≤ (↑T : ℝ) / (↑p : ℝ).
  Uses library Nat.cast_div_le.
  Lean, line 249
  have h1 : ((T / p : ℕ) : ℝ) ≤ (T : ℝ) / p := Nat.cast_div_le
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 249 at 612c41e635db ↗
  hmean.hper.hk.hc'.h2 have (↑{t ∈ Finset.range T | p ∣ b + (k + (1 : ℕ)) + Q * t}.card : ℝ) ≤ (↑(T / p) : ℝ) + (1 : ℝ)
  Leaves (↑{t ∈ Finset.range T | p ∣ b + (k + (1 : ℕ)) + Q * t}.card : ℝ) ≤ (↑T : ℝ) / (↑p : ℝ) + (1 : ℝ), with h2 : (↑{t ∈ Finset.range T | p ∣ b + (k + (1 : ℕ)) + Q * t}.card : ℝ) ≤ (↑(T / p) : ℝ) + (1 : ℝ).
  Uses library Finset.range.
  Lean, lines 250–251
  have h2 : (((Finset.range T).filter (fun t => p ∣ b + (k + 1) + Q * t)).card : ℝ) ≤ ((T / p : ℕ) : ℝ) + 1 := by exact_mod_cast hc
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 250–251 at 612c41e635db ↗
  hmean.hper.s4 calc ∑' (k : ℕ), ∑ t ∈ Finset.range T, (if p ∣ b + Q * t + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)) ≤ ∑' (k : ℕ), ((↑T : ℝ) / (↑p : ℝ) + (1 : ℝ)) * ((1 : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)))
  Closes the goal.
  Uses library Finset.range, Summable.tsum_le_tsum, summable_sum.
  Lean, lines 255–258
  calc ∑' k : ℕ, ∑ t ∈ Finset.range T, (if p ∣ b + Q * t + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1) ≤ ∑' k : ℕ, ((T : ℝ) / p + 1) * (1 / 2 ^ (k + 1)) := Summable.tsum_le_tsum hk (summable_sum (fun t _ => hind p t)) (hS2.mul_left _)
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 255–258 at 612c41e635db ↗
  hmean.hper.s5 calc
  Closes the goal.
  Uses library tsum_mul_left, mul_one.
  Lean, line 259
  _ = (T : ℝ) / p + 1 := by rw [tsum_mul_left, hsum1, mul_one]
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 259 at 612c41e635db ↗
7. hmean.hppos have (0 : ℝ) < (↑p : ℝ)
  Leaves ∑ x ∈ Finset.range T, ∑' (k : ℕ), (if p ∣ b + Q * x + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)) ≤ ((1 : ℝ) / (↑p : ℝ) + (1 : ℝ) / (↑T : ℝ)) * (↑T : ℝ), with hppos : (0 : ℝ) < (↑p : ℝ).
  Uses library Nat.prime_of_mem_primeFactors.
  Lean, line 262
  have hppos : (0 : ℝ) < p := by exact_mod_cast (Nat.prime_of_mem_primeFactors hp).pos
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 262 at 612c41e635db ↗
8. hmean.s8 calc ∑ t ∈ Finset.range T, ∑' (k : ℕ), (if p ∣ b + Q * t + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)) ≤ (↑T : ℝ) / (↑p : ℝ) + (1 : ℝ)
  Closes the goal.
  Uses library Finset.range.
  Lean, lines 263–265
  calc ∑ t ∈ Finset.range T, ∑' k : ℕ, (if p ∣ b + Q * t + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1) ≤ (T : ℝ) / p + 1 := hper p hp
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 263–265 at 612c41e635db ↗
9. hmean.s9 calc routine: field_simp
  Closes the goal.
  Lean, line 266
  _ = ((1 : ℝ) / p + 1 / T) * T := by field_simp
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 266 at 612c41e635db ↗
hTpos have (0 : ℝ) < (↑T : ℝ)
Leaves (∑ t ∈ Finset.range T, |(↑q : ℝ) * ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (b + Q * t + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) - (↑(round ((↑q : ℝ) * ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (b + Q * t + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)))) : ℝ)|) / (↑T : ℝ) ≤ (↑q : ℝ) * ∑ p ∈ a.primeFactors, ((1 : ℝ) / (↑p : ℝ) + (1 : ℝ) / (↑T : ℝ)), with hTpos : (0 : ℝ) < (↑T : ℝ).
Lean, line 267
```
  have hTpos : (0 : ℝ) < T := by exact_mod_cast hT
```
targets/erdos-69/nodes/spec-84446025/Proof.lean, line 267 at 612c41e635db ↗
hq0 have (0 : ℝ) ≤ (↑q : ℝ) routine: positivity
Leaves (∑ t ∈ Finset.range T, |(↑q : ℝ) * ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (b + Q * t + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) - (↑(round ((↑q : ℝ) * ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (b + Q * t + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)))) : ℝ)|) / (↑T : ℝ) ≤ (↑q : ℝ) * ∑ p ∈ a.primeFactors, ((1 : ℝ) / (↑p : ℝ) + (1 : ℝ) / (↑T : ℝ)), with hq0 : (0 : ℝ) ≤ (↑q : ℝ).
Lean, line 268
```
  have hq0 : (0 : ℝ) ≤ q := by positivity
```
targets/erdos-69/nodes/spec-84446025/Proof.lean, line 268 at 612c41e635db ↗
hpt have ∀ (t : ℕ), |(↑q : ℝ) * ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (b + Q * t + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) - (↑(round ((↑q : ℝ) * ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (b + Q * t + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)))) : ℝ)| ≤ (↑q : ℝ) * ∑ p ∈ a.primeFactors, ∑' (k : ℕ), (if p ∣ b + Q * t + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ))
Leaves (∑ t ∈ Finset.range T, |(↑q : ℝ) * ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (b + Q * t + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) - (↑(round ((↑q : ℝ) * ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (b + Q * t + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)))) : ℝ)|) / (↑T : ℝ) ≤ (↑q : ℝ) * ∑ p ∈ a.primeFactors, ((1 : ℝ) / (↑p : ℝ) + (1 : ℝ) / (↑T : ℝ)), with hpt : ∀ (t : ℕ), |(↑q : ℝ) * ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (b + Q * t + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) - (↑(round ((↑q : ℝ) * ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (b + Q * t + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)))) : ℝ)| ≤ (↑q : ℝ) * ∑ p ∈ a.primeFactors, ∑' (k : ℕ), (if p ∣ b + Q * t + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)).
Uses library round, mul_add, abs_neg, abs_of_nonneg, mul_nonneg.
Lean, lines 270–286
```
  have hpt : ∀ t : ℕ,
      |(q : ℝ) * ∑' k : ℕ, (ω (a * (b + Q * t + (k + 1))) : ℝ) / 2 ^ (k + 1)
        - round ((q : ℝ) * ∑' k : ℕ, (ω (a * (b + Q * t + (k + 1))) : ℝ) / 2 ^ (k + 1))|
      ≤ (q : ℝ) * ∑ p ∈ a.primeFactors,
          ∑' k : ℕ, (if p ∣ b + Q * t + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1) := by
    intro t
    obtain ⟨n, hn⟩ := hrat (b + Q * t)
    have hC : 0 ≤ ∑ p ∈ a.primeFactors,
        ∑' k : ℕ, (if p ∣ b + Q * t + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1) :=
      Finset.sum_nonneg (fun p _ => tsum_nonneg (fun k => by split_ifs <;> positivity))
    have hr := round_le ((q : ℝ) * ∑' k : ℕ, (ω (a * (b + Q * t + (k + 1))) : ℝ) / 2 ^ (k + 1)) n
    refine hr.trans ?_
    rw [mul_add] at hn
    rw [show (q : ℝ) * ∑' k : ℕ, (ω (a * (b + Q * t + (k + 1))) : ℝ) / 2 ^ (k + 1) - n
        = -((q : ℝ) * ∑ p ∈ a.primeFactors,
            ∑' k : ℕ, (if p ∣ b + Q * t + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1)) by linarith,
      abs_neg, abs_of_nonneg (mul_nonneg hq0 hC)]
```
targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 270–286 at 612c41e635db ↗
1. hpt.s1 obtain ∃ (t_1 : ℤ), (↑q : ℝ) * (∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (b + Q * t + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) + ∑ p ∈ a.primeFactors, ∑' (k : ℕ), (if p ∣ b + Q * t + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ))) = (↑t_1 : ℝ)
  Leaves |(↑q : ℝ) * ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (b + Q * t + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) - (↑(round ((↑q : ℝ) * ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (b + Q * t + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)))) : ℝ)| ≤ (↑q : ℝ) * ∑ p ∈ a.primeFactors, ∑' (k : ℕ), (if p ∣ b + Q * t + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)), with n : ℤ, hn : (↑q : ℝ) * (∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (b + Q * t + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) + ∑ p ∈ a.primeFactors, ∑' (k : ℕ), (if p ∣ b + Q * t + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ))) = (↑n : ℝ).
  Lean, line 276
  obtain ⟨n, hn⟩ := hrat (b + Q * t)
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 276 at 612c41e635db ↗
2. hpt.hC have (0 : ℝ) ≤ ∑ p ∈ a.primeFactors, ∑' (k : ℕ), (if p ∣ b + Q * t + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ))
  Leaves |(↑q : ℝ) * ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (b + Q * t + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) - (↑(round ((↑q : ℝ) * ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (b + Q * t + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)))) : ℝ)| ≤ (↑q : ℝ) * ∑ p ∈ a.primeFactors, ∑' (k : ℕ), (if p ∣ b + Q * t + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)), with hC : (0 : ℝ) ≤ ∑ p ∈ a.primeFactors, ∑' (k : ℕ), (if p ∣ b + Q * t + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)).
  Uses library Finset.sum_nonneg, tsum_nonneg.
  Lean, lines 277–279
  have hC : 0 ≤ ∑ p ∈ a.primeFactors, ∑' k : ℕ, (if p ∣ b + Q * t + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1) := Finset.sum_nonneg (fun p _ => tsum_nonneg (fun k => by split_ifs <;> positivity))
  targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 277–279 at 612c41e635db ↗
3. hpt.hr have |(↑q : ℝ) * ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (b + Q * t + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) - (↑(round ((↑q : ℝ) * ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (b + Q * t + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)))) : ℝ)| ≤ |(↑q : ℝ) * ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (b + Q * t + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) - (↑n : ℝ)|
  Leaves |(↑q : ℝ) * ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (b + Q * t + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) - (↑(round ((↑q : ℝ) * ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (b + Q * t + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)))) : ℝ)| ≤ (↑q : ℝ) * ∑ p ∈ a.primeFactors, ∑' (k : ℕ), (if p ∣ b + Q * t + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)), with hr : |(↑q : ℝ) * ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (b + Q * t + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) - (↑(round ((↑q : ℝ) * ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (b + Q * t + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)))) : ℝ)| ≤ |(↑q : ℝ) * ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (b + Q * t + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) - (↑n : ℝ)|.
  Uses library round_le.
  Lean, line 280
  have hr := round_le ((q : ℝ) * ∑' k : ℕ, (ω (a * (b + Q * t + (k + 1))) : ℝ) / 2 ^ (k + 1)) n
  targets/erdos-69/nodes/spec-84446025/Proof.lean, line 280 at 612c41e635db ↗
s6 calc (∑ t ∈ Finset.range T, |(↑q : ℝ) * ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (b + Q * t + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) - (↑(round ((↑q : ℝ) * ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (b + Q * t + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)))) : ℝ)|) / (↑T : ℝ) ≤ (∑ t ∈ Finset.range T, (↑q : ℝ) * ∑ p ∈ a.primeFactors, ∑' (k : ℕ), (if p ∣ b + Q * t + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ))) / (↑T : ℝ)
Closes the goal.
Uses library Finset.range, round.
Lean, lines 287–293
```
  calc (∑ t ∈ Finset.range T,
          |(q : ℝ) * ∑' k : ℕ, (ω (a * (b + Q * t + (k + 1))) : ℝ) / 2 ^ (k + 1)
            - round ((q : ℝ) * ∑' k : ℕ, (ω (a * (b + Q * t + (k + 1))) : ℝ) / 2 ^ (k + 1))|) / T
      ≤ (∑ t ∈ Finset.range T, (q : ℝ) * ∑ p ∈ a.primeFactors,
          ∑' k : ℕ, (if p ∣ b + Q * t + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1)) / T := by
        gcongr with t ht
        exact hpt t
```
targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 287–293 at 612c41e635db ↗

s7 calc

Closes the goal.

Uses library Finset.range, Finset.mul_sum, mul_div_assoc.

Lean, lines 294–296

    _ = (q : ℝ) * ((∑ t ∈ Finset.range T, ∑ p ∈ a.primeFactors,
          ∑' k : ℕ, (if p ∣ b + Q * t + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1)) / T) := by
        rw [← Finset.mul_sum, mul_div_assoc]

targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 294–296 at 612c41e635db ↗

s8 calc (↑q : ℝ) * ((∑ t ∈ Finset.range T, ∑ p ∈ a.primeFactors, ∑' (k : ℕ), (if p ∣ b + Q * t + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ))) / (↑T : ℝ)) ≤ (↑q : ℝ) * ∑ p ∈ a.primeFactors, ((1 : ℝ) / (↑p : ℝ) + (1 : ℝ) / (↑T : ℝ))
Closes the goal.
Uses library mul_le_mul_of_nonneg_left.
Lean, lines 297–298
```
    _ ≤ (q : ℝ) * ∑ p ∈ a.primeFactors, ((1 : ℝ) / p + 1 / T) :=
        mul_le_mul_of_nonneg_left hmean hq0
```
targets/erdos-69/nodes/spec-84446025/Proof.lean, lines 297–298 at 612c41e635db ↗

The proof in Lean (Proof.lean)

Checked by the kernel — these bytes are the ones its attestation names: attestations/000315.json, merge commit 612c41e635db.

Proof.lean — its sha256 is the artifact_hash of the attestation below, so these are the bytes the gate checked. Rendered from targets/erdos-69/nodes/spec-84446025/Proof.lean, sha256 7421b35be87d.

import Mathlib
import Nodes.«spec-84446025».Context

open scoped ArithmeticFunction.omega

/-! A speculative ingredient for erdos-69 (D-29): the rational side of the composite-dilation route,
packaged. Write `D_a(m) = ∑_{k ≥ 0} ω (a (m + k + 1)) / 2^(k+1)` for the tail dilated by `a`. If
`q · ∑ ω(n)/2^n` is the integer `z`, then along any progression `b + Q t` (`t < T`) with every
prime factor of `a` coprime to `Q`, the numbers `q · D_a(b + Q t)` are on average within
`q · ∑_{p ∣ a} (1/p + 1/T)` of an integer. For a rough dilation `a = 1 + P# (1 + j)` the
node `spec-e0b917d1` bounds `∑_{p ∣ a} 1/p` by `5 / log P`, so rationality forces the dilated tails
close to integers on average; the unconditional half of the route (github.com/plby/lean-proofs,
`ErdosProblems/Erdos69`; see the annex on `erdos-69`) shows a signed combination of them is not.
Proof ingredients: `ω (a n) = ω a + ω n - #{p ∣ a : p ∣ n}`, integrality of `q` times each tail,
and at most `T/p + 1` solutions `t < T` of `p ∣ c + Q t` when `p ∤ Q`. -/

theorem Opn.erdos_69_rational_dilated_tails_near_integers :
    ∀ (q : ℕ) (z : ℤ), (q : ℝ) * ∑' n : ℕ, (ω n : ℝ) / 2 ^ n = z →
      ∀ (a Q b T : ℕ), a ≠ 0 → 0 < T → (∀ p ∈ a.primeFactors, Nat.Coprime p Q) →
        (∑ t ∈ Finset.range T,
            |(q : ℝ) * ∑' k : ℕ, (ω (a * (b + Q * t + (k + 1))) : ℝ) / 2 ^ (k + 1)
              - round ((q : ℝ) * ∑' k : ℕ, (ω (a * (b + Q * t + (k + 1))) : ℝ) / 2 ^ (k + 1))|) / T
          ≤ (q : ℝ) * ∑ p ∈ a.primeFactors, ((1 : ℝ) / p + 1 / T) := by
  intro q z hz a Q b T ha hT hcop
  -- the rational side: q (dilated tail + correction) is an integer
  have hrat : ∀ m : ℕ, ∃ t : ℤ,
      (q : ℝ) * (∑' k : ℕ, (ω (a * (m + (k + 1))) : ℝ) / 2 ^ (k + 1)
        + ∑ p ∈ a.primeFactors,
            ∑' k : ℕ, (if p ∣ m + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1)) = t := by
    intro m
    have hdil : ∑' k : ℕ, (ω (a * (m + (k + 1))) : ℝ) / 2 ^ (k + 1)
        = ∑' k : ℕ, (ω (m + (k + 1)) : ℝ) / 2 ^ (k + 1) + (ω a : ℝ)
          - ∑ p ∈ a.primeFactors,
              ∑' k : ℕ, (if p ∣ m + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1) := by
      -- ω is the number of prime factors
      have hω : ∀ x : ℕ, ω x = x.primeFactors.card := fun x => by
        rw [ArithmeticFunction.cardDistinctFactors_apply]; rfl
      -- the pointwise identity ω(a n) + #{p ∣ a : p ∣ n} = ω a + ω n
      have hpt : ∀ n : ℕ, n ≠ 0 →
          (ω (a * n) : ℝ) = (ω n : ℝ) + (ω a : ℝ)
            - ∑ p ∈ a.primeFactors, (if p ∣ n then (1 : ℝ) else 0) := by
        intro n hn
        have hu : (a * n).primeFactors = a.primeFactors ∪ n.primeFactors := Nat.primeFactors_mul ha hn
        have hi : a.primeFactors ∩ n.primeFactors = a.primeFactors.filter (· ∣ n) := by
          ext p
          simp only [Finset.mem_inter, Finset.mem_filter, Nat.mem_primeFactors]
          constructor
          · rintro ⟨h1, h2⟩; exact ⟨h1, h2.2.1⟩
          · rintro ⟨h1, h2⟩; exact ⟨h1, h1.1, h2, hn⟩
        have hc := Finset.card_union_add_card_inter a.primeFactors n.primeFactors
        rw [← hu, hi] at hc
        have hs : ∑ p ∈ a.primeFactors, (if p ∣ n then (1 : ℝ) else 0)
            = ((a.primeFactors.filter (· ∣ n)).card : ℝ) := by
          rw [Finset.sum_ite, Finset.sum_const_zero, add_zero, Finset.sum_const, nsmul_eq_mul, mul_one]
        rw [hs, hω, hω, hω]
        have hc' : ((a * n).primeFactors.card : ℝ) + ((a.primeFactors.filter (· ∣ n)).card : ℝ)
            = (a.primeFactors.card : ℝ) + (n.primeFactors.card : ℝ) := by exact_mod_cast hc
        linarith
      -- summability tools
      have hgeo : ∀ c : ℝ, Summable (fun k : ℕ => ((k : ℝ) + c) * (1 / 2 : ℝ) ^ k) := by
        intro c
        have h1 := summable_pow_mul_geometric_of_norm_lt_one 1 (by norm_num [Real.norm_eq_abs] : ‖(1 / 2 : ℝ)‖ < 1)
        have h2 := (summable_geometric_of_lt_one (by norm_num : (0 : ℝ) ≤ 1 / 2) (by norm_num)).mul_left c
        refine (h1.add h2).congr (fun k => ?_)
        simp only [pow_one]; ring
      have hw : ∀ k : ℕ, (1 : ℝ) / 2 ^ (k + 1) ≤ (1 / 2 : ℝ) ^ k := by
        intro k
        rw [one_div_pow, pow_succ]
        apply one_div_le_one_div_of_le (by positivity)
        linarith [pow_pos (by norm_num : (0 : ℝ) < 2) k]
      have hωle : ∀ x : ℕ, (ω x : ℝ) ≤ x + 1 := by
        intro x
        have h1 : ω x ≤ x + 1 := by
          rw [hω]
          calc x.primeFactors.card ≤ (Finset.range (x + 1)).card :=
                Finset.card_le_card (fun p hp =>
                  Finset.mem_range.2 (Nat.lt_succ_of_le (Nat.le_of_mem_primeFactors hp)))
            _ = x + 1 := Finset.card_range _
        exact_mod_cast h1
      have hS1 : Summable (fun k : ℕ => (ω (m + (k + 1)) : ℝ) / 2 ^ (k + 1)) := by
        refine Summable.of_nonneg_of_le (fun k => by positivity) (fun k => ?_) (hgeo ((m : ℝ) + 2))
        have h1 := hωle (m + (k + 1))
        have h2 := hw k
        have h3 : (0 : ℝ) ≤ (ω (m + (k + 1)) : ℝ) := by positivity
        calc (ω (m + (k + 1)) : ℝ) / 2 ^ (k + 1) = (ω (m + (k + 1)) : ℝ) * (1 / 2 ^ (k + 1)) := by ring
          _ ≤ ((k : ℝ) + ((m : ℝ) + 2)) * (1 / 2 : ℝ) ^ k := by
            apply mul_le_mul _ h2 (by positivity) (by positivity)
            push_cast at h1; linarith
      have hS2 : Summable (fun k : ℕ => (1 : ℝ) / 2 ^ (k + 1)) := by
        refine Summable.of_nonneg_of_le (fun k => by positivity) hw ?_
        exact summable_geometric_of_lt_one (by norm_num) (by norm_num)
      have hS3 : ∀ p : ℕ, Summable (fun k : ℕ => (if p ∣ m + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1)) := by
        intro p
        refine Summable.of_nonneg_of_le (fun k => by split_ifs <;> positivity) (fun k => ?_) hS2
        split_ifs <;> simp
      have hsum1 : ∑' k : ℕ, (1 : ℝ) / 2 ^ (k + 1) = 1 := by
        have : (fun k : ℕ => (1 : ℝ) / 2 ^ (k + 1)) = fun k => (1 / 2) * (1 / 2 : ℝ) ^ k := by
          funext k; rw [pow_succ, one_div_pow]; field_simp
        rw [this, tsum_mul_left, tsum_geometric_two]; norm_num
      -- assemble
      have hterm : ∀ k : ℕ, (ω (a * (m + (k + 1))) : ℝ) / 2 ^ (k + 1)
          = (ω (m + (k + 1)) : ℝ) / 2 ^ (k + 1) + (ω a : ℝ) * (1 / 2 ^ (k + 1))
            - ∑ p ∈ a.primeFactors, (if p ∣ m + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1) := by
        intro k
        rw [hpt (m + (k + 1)) (by omega), ← Finset.sum_div]
        ring
      rw [tsum_congr hterm, Summable.tsum_sub (hS1.add (hS2.mul_left _)) (summable_sum (fun p _ => hS3 p)),
        Summable.tsum_add hS1 (hS2.mul_left _), tsum_mul_left, hsum1, mul_one,
        Summable.tsum_finsetSum (fun p _ => hS3 p)]
    -- integrality of q times the plain tail
    have hbound : ∀ n : ℕ,
        (ω n : ℝ) / 2 ^ n ≤ (n : ℝ) ^ 1 * (1 / 2 : ℝ) ^ n + (1 / 2 : ℝ) ^ n := by
      intro n
      have h1 : ω n ≤ n + 1 := by
        rw [ArithmeticFunction.cardDistinctFactors_apply]
        calc n.primeFactorsList.dedup.length = n.primeFactors.card := rfl
          _ ≤ (Finset.range (n + 1)).card :=
              Finset.card_le_card (fun p hp =>
                Finset.mem_range.2 (Nat.lt_succ_of_le (Nat.le_of_mem_primeFactors hp)))
          _ = n + 1 := Finset.card_range _
      have h2 : (ω n : ℝ) ≤ (n : ℝ) + 1 := by exact_mod_cast h1
      have h4 : (0 : ℝ) ≤ ((2 : ℝ) ^ n)⁻¹ := by positivity
      rw [pow_one, one_div, inv_pow, div_eq_mul_inv]
      nlinarith [mul_le_mul_of_nonneg_right h2 h4]
    have hsum : Summable (fun n : ℕ => (ω n : ℝ) / 2 ^ n) := by
      refine Summable.of_nonneg_of_le (fun n => by positivity) hbound ?_
      exact (summable_pow_mul_geometric_of_norm_lt_one 1 (by norm_num [Real.norm_eq_abs])).add
        (summable_geometric_of_lt_one (by norm_num) (by norm_num))
    have htail : ∑' k : ℕ, (ω (m + (k + 1)) : ℝ) / 2 ^ (k + 1)
        = 2 ^ m * (∑' n : ℕ, (ω n : ℝ) / 2 ^ n
            - ∑ n ∈ Finset.range (m + 1), (ω n : ℝ) / 2 ^ n) := by
      have h := hsum.sum_add_tsum_nat_add (m + 1)
      have h2 : ∑' i : ℕ, (ω (i + (m + 1)) : ℝ) / 2 ^ (i + (m + 1))
          = (∑' k : ℕ, (ω (m + (k + 1)) : ℝ) / 2 ^ (k + 1)) / 2 ^ m := by
        rw [← tsum_div_const]
        refine tsum_congr (fun k => ?_)
        rw [show k + (m + 1) = m + (k + 1) by ring, show m + (k + 1) = (k + 1) + m by ring,
          pow_add, div_div]
      rw [h2] at h
      have h3 := eq_sub_of_add_eq' h
      rw [← h3]
      field_simp
    have hA : ∑ n ∈ Finset.range (m + 1), (q : ℝ) * (ω n : ℝ) * 2 ^ (m - n)
        = 2 ^ m * ((q : ℝ) * ∑ n ∈ Finset.range (m + 1), (ω n : ℝ) / 2 ^ n) := by
      rw [Finset.mul_sum, Finset.mul_sum]
      refine Finset.sum_congr rfl (fun n hn => ?_)
      have hn' : n ≤ m := Nat.lt_succ_iff.1 (Finset.mem_range.1 hn)
      rw [pow_sub₀ (2 : ℝ) two_ne_zero hn']
      field_simp
    refine ⟨2 ^ m * z - ∑ n ∈ Finset.range (m + 1), (q : ℤ) * ω n * 2 ^ (m - n) + q * ω a, ?_⟩
    push_cast
    rw [hdil, sub_add_cancel, htail]
    linear_combination (2 : ℝ) ^ m * hz + hA
  -- the mean of the correction along the progression
  have hmean : (∑ t ∈ Finset.range T, ∑ p ∈ a.primeFactors,
          ∑' k : ℕ, (if p ∣ b + Q * t + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1)) / T
        ≤ ∑ p ∈ a.primeFactors, ((1 : ℝ) / p + 1 / T) := by
    have hcount : ∀ (p Q c T : ℕ), p.Prime → Nat.Coprime p Q →
        ((Finset.range T).filter (fun t => p ∣ c + Q * t)).card ≤ T / p + 1 := by
      intro p Q c T hp hQ
      have hp0 : 0 < p := hp.pos
      have key := Finset.card_le_card_of_injOn (s := (Finset.range T).filter (fun t => p ∣ c + Q * t))
        (t := Finset.range (T / p + 1)) (fun t => t / p) ?_ ?_
      · simpa using key
      · intro t ht
        have ht1 : t < T := (Finset.mem_range.1 (Finset.mem_filter.1 ht).1)
        exact Finset.mem_coe.2 (Finset.mem_range.2 (Nat.lt_succ_of_le (Nat.div_le_div_right ht1.le)))
      · intro t ht t' ht' heq
        have ht := Finset.mem_filter.1 (Finset.mem_coe.1 ht)
        have ht' := Finset.mem_filter.1 (Finset.mem_coe.1 ht')
        rw [Finset.mem_range] at ht ht'
        have heq' : t / p = t' / p := heq
        -- p ∣ Q * (t - t') in ℤ
        have hz : (p : ℤ) ∣ (Q : ℤ) * ((t : ℤ) - t') := by
          have h1 : (p : ℤ) ∣ (c : ℤ) + Q * t := by exact_mod_cast ht.2
          have h2 : (p : ℤ) ∣ (c : ℤ) + Q * t' := by exact_mod_cast ht'.2
          have := dvd_sub h1 h2
          have e : (c : ℤ) + Q * t - (c + Q * t') = Q * (t - t') := by ring
          rwa [e] at this
        have hpQ : ¬ (p : ℤ) ∣ Q := by
          intro h
          have : p ∣ Q := by exact_mod_cast h
          have := Nat.Coprime.eq_one_of_dvd hQ this
          exact hp.one_lt.ne' this
        have hpd : (p : ℤ) ∣ (t : ℤ) - t' :=
          (Int.Prime.dvd_mul' hp hz).resolve_left hpQ
        -- |t - t'| < p
        have hlt1 : (t : ℤ) - t' < p := by
          have a1 := Nat.div_add_mod t p
          have a2 := Nat.div_add_mod t' p
          have b1 := Nat.mod_lt t hp0
          have b2 := Nat.mod_lt t' hp0
          rw [heq'] at a1
          omega
        have hlt2 : (t' : ℤ) - t < p := by
          have a1 := Nat.div_add_mod t p
          have a2 := Nat.div_add_mod t' p
          have b1 := Nat.mod_lt t hp0
          have b2 := Nat.mod_lt t' hp0
          rw [heq'] at a1
          omega
        obtain ⟨k, hk⟩ := hpd
        have hp' : (0 : ℤ) < p := by exact_mod_cast hp0
        have : k = 0 := by
          rcases lt_trichotomy k 0 with h | h | h
          · nlinarith
          · exact h
          · nlinarith
        rw [this, mul_zero] at hk
        omega
    have hTpos : (0 : ℝ) < T := by exact_mod_cast hT
    have hS2 : Summable (fun k : ℕ => (1 : ℝ) / 2 ^ (k + 1)) := by
      refine Summable.of_nonneg_of_le (fun k => by positivity) (fun k => ?_)
        (summable_geometric_of_lt_one (by norm_num : (0 : ℝ) ≤ 1 / 2) (by norm_num))
      rw [one_div_pow, pow_succ]
      apply one_div_le_one_div_of_le (by positivity)
      linarith [pow_pos (by norm_num : (0 : ℝ) < 2) k]
    have hsum1 : ∑' k : ℕ, (1 : ℝ) / 2 ^ (k + 1) = 1 := by
      have : (fun k : ℕ => (1 : ℝ) / 2 ^ (k + 1)) = fun k => (1 / 2) * (1 / 2 : ℝ) ^ k := by
        funext k; rw [pow_succ, one_div_pow]; field_simp
      rw [this, tsum_mul_left, tsum_geometric_two]; norm_num
    have hind : ∀ (p t : ℕ), Summable (fun k : ℕ =>
        (if p ∣ b + Q * t + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1)) := by
      intro p t
      refine Summable.of_nonneg_of_le (fun k => by split_ifs <;> positivity) (fun k => ?_) hS2
      split_ifs <;> simp
    -- one prime at a time
    have hper : ∀ p ∈ a.primeFactors, ∑ t ∈ Finset.range T,
        ∑' k : ℕ, (if p ∣ b + Q * t + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1)
          ≤ (T : ℝ) / p + 1 := by
      intro p hp
      have hpp : p.Prime := Nat.prime_of_mem_primeFactors hp
      have hppos : (0 : ℝ) < p := by exact_mod_cast hpp.pos
      rw [← Summable.tsum_finsetSum (fun t _ => hind p t)]
      have hk : ∀ k : ℕ, ∑ t ∈ Finset.range T,
          (if p ∣ b + Q * t + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1)
            ≤ ((T : ℝ) / p + 1) * (1 / 2 ^ (k + 1)) := by
        intro k
        rw [← Finset.sum_div, Finset.sum_boole]
        have hc := hcount p Q (b + (k + 1)) T hpp (hcop p hp)
        have hfe : (Finset.range T).filter (fun t => p ∣ b + Q * t + (k + 1))
            = (Finset.range T).filter (fun t => p ∣ b + (k + 1) + Q * t) := by
          apply Finset.filter_congr
          intro t _
          rw [show b + Q * t + (k + 1) = b + (k + 1) + Q * t by ring]
        rw [hfe]
        have hc' : (((Finset.range T).filter (fun t => p ∣ b + (k + 1) + Q * t)).card : ℝ)
            ≤ (T : ℝ) / p + 1 := by
          have h1 : ((T / p : ℕ) : ℝ) ≤ (T : ℝ) / p := Nat.cast_div_le
          have h2 : (((Finset.range T).filter (fun t => p ∣ b + (k + 1) + Q * t)).card : ℝ)
              ≤ ((T / p : ℕ) : ℝ) + 1 := by exact_mod_cast hc
          linarith
        rw [div_eq_mul_one_div]
        exact mul_le_mul_of_nonneg_right hc' (by positivity)
      calc ∑' k : ℕ, ∑ t ∈ Finset.range T,
            (if p ∣ b + Q * t + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1)
          ≤ ∑' k : ℕ, ((T : ℝ) / p + 1) * (1 / 2 ^ (k + 1)) :=
            Summable.tsum_le_tsum hk (summable_sum (fun t _ => hind p t)) (hS2.mul_left _)
        _ = (T : ℝ) / p + 1 := by rw [tsum_mul_left, hsum1, mul_one]
    rw [div_le_iff₀ hTpos, Finset.sum_comm, Finset.sum_mul]
    refine Finset.sum_le_sum (fun p hp => ?_)
    have hppos : (0 : ℝ) < p := by exact_mod_cast (Nat.prime_of_mem_primeFactors hp).pos
    calc ∑ t ∈ Finset.range T,
          ∑' k : ℕ, (if p ∣ b + Q * t + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1)
        ≤ (T : ℝ) / p + 1 := hper p hp
      _ = ((1 : ℝ) / p + 1 / T) * T := by field_simp
  have hTpos : (0 : ℝ) < T := by exact_mod_cast hT
  have hq0 : (0 : ℝ) ≤ q := by positivity
  -- pointwise: the distance to the nearest integer is at most q times the correction
  have hpt : ∀ t : ℕ,
      |(q : ℝ) * ∑' k : ℕ, (ω (a * (b + Q * t + (k + 1))) : ℝ) / 2 ^ (k + 1)
        - round ((q : ℝ) * ∑' k : ℕ, (ω (a * (b + Q * t + (k + 1))) : ℝ) / 2 ^ (k + 1))|
      ≤ (q : ℝ) * ∑ p ∈ a.primeFactors,
          ∑' k : ℕ, (if p ∣ b + Q * t + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1) := by
    intro t
    obtain ⟨n, hn⟩ := hrat (b + Q * t)
    have hC : 0 ≤ ∑ p ∈ a.primeFactors,
        ∑' k : ℕ, (if p ∣ b + Q * t + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1) :=
      Finset.sum_nonneg (fun p _ => tsum_nonneg (fun k => by split_ifs <;> positivity))
    have hr := round_le ((q : ℝ) * ∑' k : ℕ, (ω (a * (b + Q * t + (k + 1))) : ℝ) / 2 ^ (k + 1)) n
    refine hr.trans ?_
    rw [mul_add] at hn
    rw [show (q : ℝ) * ∑' k : ℕ, (ω (a * (b + Q * t + (k + 1))) : ℝ) / 2 ^ (k + 1) - n
        = -((q : ℝ) * ∑ p ∈ a.primeFactors,
            ∑' k : ℕ, (if p ∣ b + Q * t + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1)) by linarith,
      abs_neg, abs_of_nonneg (mul_nonneg hq0 hC)]
  calc (∑ t ∈ Finset.range T,
          |(q : ℝ) * ∑' k : ℕ, (ω (a * (b + Q * t + (k + 1))) : ℝ) / 2 ^ (k + 1)
            - round ((q : ℝ) * ∑' k : ℕ, (ω (a * (b + Q * t + (k + 1))) : ℝ) / 2 ^ (k + 1))|) / T
      ≤ (∑ t ∈ Finset.range T, (q : ℝ) * ∑ p ∈ a.primeFactors,
          ∑' k : ℕ, (if p ∣ b + Q * t + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1)) / T := by
        gcongr with t ht
        exact hpt t
    _ = (q : ℝ) * ((∑ t ∈ Finset.range T, ∑ p ∈ a.primeFactors,
          ∑' k : ℕ, (if p ∣ b + Q * t + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1)) / T) := by
        rw [← Finset.mul_sum, mul_div_assoc]
    _ ≤ (q : ℝ) * ∑ p ∈ a.primeFactors, ((1 : ℝ) / p + 1 / T) :=
        mul_le_mul_of_nonneg_left hmean hq0

What is known

Work on it

No explainer yet. This proof written as a journal would print it, labelled unverified, is the next thing a writer could add, by pull request (D-3, D-36; the guide shows how).

Write the explainer →

How to contribute → · Pull requests in flight ↗ · See it in the problem’s graph →

Record

Statement: the Lean file and its words (1 version)

Statement not audited — only a problem’s root statement is audited for fidelity (D-9); the kernel checks a proof against this Lean as written.

import Mathlib
import Nodes.«spec-84446025».Context

open scoped ArithmeticFunction.omega

/-! A speculative ingredient for erdos-69 (D-29): the rational side of the composite-dilation route,
packaged. Write `D_a(m) = ∑_{k ≥ 0} ω (a (m + k + 1)) / 2^(k+1)` for the tail dilated by `a`. If
`q · ∑ ω(n)/2^n` is the integer `z`, then along any progression `b + Q t` (`t < T`) with every
prime factor of `a` coprime to `Q`, the numbers `q · D_a(b + Q t)` are on average within
`q · ∑_{p ∣ a} (1/p + 1/T)` of an integer. For a rough dilation `a = 1 + P# (1 + j)` the
node `spec-e0b917d1` bounds `∑_{p ∣ a} 1/p` by `5 / log P`, so rationality forces the dilated tails
close to integers on average; the unconditional half of the route (github.com/plby/lean-proofs,
`ErdosProblems/Erdos69`; see the annex on `erdos-69`) shows a signed combination of them is not.
Proof ingredients: `ω (a n) = ω a + ω n - #{p ∣ a : p ∣ n}`, integrality of `q` times each tail,
and at most `T/p + 1` solutions `t < T` of `p ∣ c + Q t` when `p ∤ Q`. -/

theorem Opn.erdos_69_rational_dilated_tails_near_integers :
    ∀ (q : ℕ) (z : ℤ), (q : ℝ) * ∑' n : ℕ, (ω n : ℝ) / 2 ^ n = z →
      ∀ (a Q b T : ℕ), a ≠ 0 → 0 < T → (∀ p ∈ a.primeFactors, Nat.Coprime p Q) →
        (∑ t ∈ Finset.range T,
            |(q : ℝ) * ∑' k : ℕ, (ω (a * (b + Q * t + (k + 1))) : ℝ) / 2 ^ (k + 1)
              - round ((q : ℝ) * ∑' k : ℕ, (ω (a * (b + Q * t + (k + 1))) : ℝ) / 2 ^ (k + 1))|) / T
          ≤ (q : ℝ) * ∑ p ∈ a.primeFactors, ((1 : ℝ) / p + 1 / T) := by
  sorry

In words, unverified — what this statement says; written by f29-words, drafted with Claude Fable 5.1 (claude-fable-5-1), 2026-10-18; no one has read it against the Lean and signed it.

Draft · drafted, by the model named above

Rendered from gloss/a91cb15b1ef8….md · Improve these words →

Rendered from targets/erdos-69/nodes/spec-84446025/Statement.lean. Origin: authored.

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000315.json, merge commit 612c41e635db.

Verdict pass, from attestations/000315.json.

Submitter: t0929-3
Toolchain: leanprover/lean4:v4.33.1 (hash f54d0bc916bf76a7fae460ce9d078ccd1f74aeb4fd12c4b6546bca28b6aa1c63)
Mathlib: 0df444a360eaa60ab8c11dca51a86af692955474
Reviewer: none needed (calibration)

Step	Check	Result
1	toolchain	pass
2	paths	pass
4	kernel-replay	pass
5	axioms	pass
6	hazards	pass
7	witness	pass
8	deps	pass

Witness

Checked by the kernel — step 7 passed in the run its attestation records: attestations/000315.json, merge commit 612c41e635db.

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/erdos-69/nodes/spec-84446025/Witness.lean, sha256 4a7bf290df2f.

import Mathlib

open scoped ArithmeticFunction.omega

theorem witness : ∃ (q : ℕ) (z : ℤ) (a Q b T : ℕ),
    (q : ℝ) * ∑' n : ℕ, (ω n : ℝ) / 2 ^ n = (z : ℝ) ∧ a ≠ 0 ∧ 0 < T ∧
      ∀ p ∈ a.primeFactors, Nat.Coprime p Q :=
  ⟨0, 0, 1, 1, 0, 1, by simp, one_ne_zero, one_pos, by simp⟩

No gloss yet: no one has written in words what this witness says (D-3 v3.30); the Lean above is the witness. How to write one →

Acknowledged findings (5)