Open Proof Network

Problems / erdos-69 / spec-9f8cb4ea

Closed form for the dilated tail

spec-9f8cb4ea Opn.erdos_69_dilated_tail_closed

proved

Proposed by a contributor.

$\displaystyle \forall a,m\in\mathbb{N},\ a\ne 0:\quad \sum_{k=0}^{\infty}\frac{\omega\bigl(a(m+k+1)\bigr)}{2^{k+1}} = \sum_{k=0}^{\infty}\frac{\omega(m+k+1)}{2^{k+1}} + \omega(a) - \sum_{p\mid a}\frac{2^{\,m \bmod p}}{2^{p}-1}$

For a nonzero natural a and any natural m, the tail of ω along the multiples a(m+k+1) equals the undilated tail plus ω(a) minus, for each prime factor p of a, 2^{m mod p}/(2^p − 1), all in ℝ, with ω(n) the number of distinct prime factors of n and the last sum over a.primeFactors. Every series is Mathlib's tsum over ℝ, which is 0 when the family is not summable.

unverified · history

Lean
theorem Opn.erdos_69_dilated_tail_closed :
    ∀ (a m : ℕ), a ≠ 0 →
      ∑' k : ℕ, (ω (a * (m + (k + 1))) : ℝ) / 2 ^ (k + 1)
        = ∑' k : ℕ, (ω (m + (k + 1)) : ℝ) / 2 ^ (k + 1) + (ω a : ℝ)
          - ∑ p ∈ a.primeFactors, (2 : ℝ) ^ (m % p) / (2 ^ p - 1) := 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, 000313, records the gate’s run.

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000313.json, merge commit f1ffb04f57f2.

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.

  1. hcl have ∀ (p m : ℕ), (0 : ℕ) < p → ∑' (k : ℕ), (if p ∣ m + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)) = (2 : ℝ) ^ (m % p) / ((2 : ℝ) ^ p - (1 : ℝ))

    Leaves ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (m + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) = ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (m + (k + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) + (↑((ω : ℕ → ℕ) a) : ℝ) - ∑ p ∈ a.primeFactors, (2 : ℝ) ^ (m % p) / ((2 : ℝ) ^ p - (1 : ℝ)), with hcl : ∀ (p m : ℕ), (0 : ℕ) < p → ∑' (k : ℕ), (if p ∣ m + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)) = (2 : ℝ) ^ (m % p) / ((2 : ℝ) ^ p - (1 : ℝ)).

    Uses library one_div_pow.

    Lean, lines 25–79
      have hcl : ∀ (p m : ℕ), 0 < p →
      ∑' k : ℕ, (if p ∣ m + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1)
        = 2 ^ (m % p) / (2 ^ p - 1) := by
    intro p m hp
    obtain ⟨s, hs⟩ : ∃ s, s = m % p := ⟨_, rfl⟩
    obtain ⟨Q, hQ⟩ : ∃ Q, Q = m / p := ⟨_, rfl⟩
    have hsp : s < p := hs ▸ Nat.mod_lt _ hp
    have hm : m = s + p * Q := by rw [hs, hQ]; exact (Nat.mod_add_div m p).symm
    rw [← hs]
    obtain ⟨k0, hk0⟩ : ∃ k0, k0 = p - 1 - s := ⟨_, rfl⟩
    have hdiv : ∀ k : ℕ, p ∣ m + (k + 1) ↔ ∃ t, k0 + p * t = k := by
      intro k
      constructor
      · rintro ⟨c, hc⟩
        have hcQ : Q < c := by
          have : p * Q < p * c := by omega
          exact Nat.lt_of_mul_lt_mul_left this
        obtain ⟨e, he⟩ : ∃ e, c = Q + 1 + e := ⟨c - Q - 1, by omega⟩
        refine ⟨e, ?_⟩
        rw [he, mul_add, mul_add, mul_one] at hc
        omega
      · rintro ⟨t, rfl⟩
        exact ⟨Q + 1 + t, by rw [mul_add, mul_add, mul_one]; omega⟩
    let f : ℕ → ℝ := fun k => (if p ∣ m + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1)
    let g : ℕ → ℕ := fun t => k0 + p * t
    have hg : Function.Injective g := by
      intro t t' h
      have : p * t = p * t' := by simp only [g] at h; omega
      exact Nat.eq_of_mul_eq_mul_left hp this
    have hzero : ∀ x ∉ Set.range g, f x = 0 := by
      intro x hx
      have : ¬ p ∣ m + (x + 1) := fun h => hx ((hdiv x).1 h)
      simp only [f, if_neg this, zero_div]
    have hcomp : f ∘ g = fun t : ℕ => (1 / 2 : ℝ) ^ (k0 + 1) * ((1 / 2 : ℝ) ^ p) ^ t := by
      funext t
      have h1 : p ∣ m + (g t + 1) := (hdiv (g t)).2 ⟨t, rfl⟩
      simp only [Function.comp, f, if_pos h1, g]
      rw [← pow_mul, ← pow_add, one_div_pow, one_div]
      ring
    have hr0 : (0 : ℝ) ≤ (1 / 2 : ℝ) ^ p := by positivity
    have hr1 : (1 / 2 : ℝ) ^ p < 1 := pow_lt_one₀ (by norm_num) (by norm_num) hp.ne'
    have hgeo := (hasSum_geometric_of_lt_one hr0 hr1).mul_left ((1 / 2 : ℝ) ^ (k0 + 1))
    rw [← hcomp] at hgeo
    have hH := (hg.hasSum_iff hzero).1 hgeo
    change ∑' k : ℕ, f k = _
    rw [hH.tsum_eq]
    have hk : k0 + 1 = p - s := by omega
    rw [hk]
    have h2 : (2 : ℝ) ^ p = 2 ^ (p - s) * 2 ^ s := by rw [← pow_add, Nat.sub_add_cancel hsp.le]
    have h3 : (1 : ℝ) < 2 ^ p := one_lt_pow₀ (by norm_num) hp.ne'
    have h4 : (2 : ℝ) ^ p - 1 ≠ 0 := by linarith
    have h5 : (0 : ℝ) < 2 ^ (p - s) := by positivity
    rw [one_div_pow, one_div_pow]
    field_simp
    rw [h2]

    targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, lines 25–79 at f1ffb04f57f2 ↗

    1. hcl.s1 obtain ∃ (s : ℕ), s = m % p

      Leaves ∑' (k : ℕ), (if p ∣ m + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)) = (2 : ℝ) ^ (m % p) / ((2 : ℝ) ^ p - (1 : ℝ)), with s : ℕ, hs : s = m % p.

      Uses library Exists.intro Existential introduction. , rfl rfl : a = a is the unique constructor of the equality type. .

      Lean, line 29
          obtain ⟨s, hs⟩ : ∃ s, s = m % p := ⟨_, rfl⟩

      targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, line 29 at f1ffb04f57f2 ↗

    2. hcl.s2 obtain ∃ (Q : ℕ), Q = m / p

      Leaves ∑' (k : ℕ), (if p ∣ m + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)) = (2 : ℝ) ^ (m % p) / ((2 : ℝ) ^ p - (1 : ℝ)), with Q : ℕ, hQ : Q = m / p.

      Uses library Exists.intro Existential introduction. , rfl rfl : a = a is the unique constructor of the equality type. .

      Lean, line 30
          obtain ⟨Q, hQ⟩ : ∃ Q, Q = m / p := ⟨_, rfl⟩

      targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, line 30 at f1ffb04f57f2 ↗

    3. hcl.hsp have s < p

      Leaves ∑' (k : ℕ), (if p ∣ m + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)) = (2 : ℝ) ^ (m % p) / ((2 : ℝ) ^ p - (1 : ℝ)), with hsp : s < p.

      Uses library Nat.mod_lt.

      Lean, line 31
          have hsp : s < p := hs ▸ Nat.mod_lt _ hp

      targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, line 31 at f1ffb04f57f2 ↗

    4. hcl.hm have m = s + p * Q

      Leaves ∑' (k : ℕ), (if p ∣ m + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)) = (2 : ℝ) ^ (m % p) / ((2 : ℝ) ^ p - (1 : ℝ)), with hm : m = s + p * Q.

      Uses library Nat.mod_add_div.

      Lean, line 32
          have hm : m = s + p * Q := by rw [hs, hQ]; exact (Nat.mod_add_div m p).symm

      targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, line 32 at f1ffb04f57f2 ↗

    5. hcl.s5 obtain ∃ (k0 : ℕ), k0 = p - (1 : ℕ) - s

      Leaves ∑' (k : ℕ), (if p ∣ m + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)) = (2 : ℝ) ^ s / ((2 : ℝ) ^ p - (1 : ℝ)), with k0 : ℕ, hk0 : k0 = p - (1 : ℕ) - s.

      Uses library Exists.intro Existential introduction. , rfl rfl : a = a is the unique constructor of the equality type. .

      Lean, line 34
          obtain ⟨k0, hk0⟩ : ∃ k0, k0 = p - 1 - s := ⟨_, rfl⟩

      targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, line 34 at f1ffb04f57f2 ↗

    6. hcl.hdiv have ∀ (k : ℕ), p ∣ m + (k + (1 : ℕ)) ↔ ∃ (t : ℕ), k0 + p * t = k

      Leaves ∑' (k : ℕ), (if p ∣ m + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)) = (2 : ℝ) ^ s / ((2 : ℝ) ^ p - (1 : ℝ)), with hdiv : ∀ (k : ℕ), p ∣ m + (k + (1 : ℕ)) ↔ ∃ (t : ℕ), k0 + p * t = k.

      Lean, lines 35–47
          have hdiv : ∀ k : ℕ, p ∣ m + (k + 1) ↔ ∃ t, k0 + p * t = k := by
      intro k
      constructor
      · rintro ⟨c, hc⟩
        have hcQ : Q < c := by
          have : p * Q < p * c := by omega
          exact Nat.lt_of_mul_lt_mul_left this
        obtain ⟨e, he⟩ : ∃ e, c = Q + 1 + e := ⟨c - Q - 1, by omega⟩
        refine ⟨e, ?_⟩
        rw [he, mul_add, mul_add, mul_one] at hc
        omega
      · rintro ⟨t, rfl⟩
        exact ⟨Q + 1 + t, by rw [mul_add, mul_add, mul_one]; omega⟩

      targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, lines 35–47 at f1ffb04f57f2 ↗

      1. hcl.hdiv.s1 case

        Leaves p ∣ m + (k + (1 : ℕ)) → ∃ (t : ℕ), k0 + p * t = k.

        Uses library Exists.intro Existential introduction. , mul_add Alias of left_distrib. , mul_one.

        Lean, lines 38–45
              · rintro ⟨c, hc⟩
        have hcQ : Q < c := by
          have : p * Q < p * c := by omega
          exact Nat.lt_of_mul_lt_mul_left this
        obtain ⟨e, he⟩ : ∃ e, c = Q + 1 + e := ⟨c - Q - 1, by omega⟩
        refine ⟨e, ?_⟩
        rw [he, mul_add, mul_add, mul_one] at hc
        omega

        targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, lines 38–45 at f1ffb04f57f2 ↗

        1. hcl.hdiv.s1.hcQ have Q < c

          Leaves ∃ (t : ℕ), k0 + p * t = k, with hcQ : Q < c.

          Uses library Nat.lt_of_mul_lt_mul_left.

          Lean, lines 39–41
                  have hcQ : Q < c := by
          have : p * Q < p * c := by omega
          exact Nat.lt_of_mul_lt_mul_left this

          targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, lines 39–41 at f1ffb04f57f2 ↗

          1. hcl.hdiv.s1.hcQ.this have p * Q < p * c routine: omega

            Leaves Q < c, with this : p * Q < p * c.

            Lean, line 40
                      have : p * Q < p * c := by omega

            targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, line 40 at f1ffb04f57f2 ↗

        2. hcl.hdiv.s1.s2 obtain ∃ (e : ℕ), c = Q + (1 : ℕ) + e

          Leaves ∃ (t : ℕ), k0 + p * t = k, with e : ℕ, he : c = Q + (1 : ℕ) + e.

          Uses library Exists.intro Existential introduction. .

          Lean, line 42
                  obtain ⟨e, he⟩ : ∃ e, c = Q + 1 + e := ⟨c - Q - 1, by omega⟩

          targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, line 42 at f1ffb04f57f2 ↗

      2. hcl.hdiv.s2 case

        Leaves (∃ (t : ℕ), k0 + p * t = k) → p ∣ m + (k + (1 : ℕ)).

        Uses library Exists.intro Existential introduction. , mul_add Alias of left_distrib. , mul_one.

        Lean, lines 46–47
              · rintro ⟨t, rfl⟩
        exact ⟨Q + 1 + t, by rw [mul_add, mul_add, mul_one]; omega⟩

        targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, lines 46–47 at f1ffb04f57f2 ↗

    7. hcl.hg have Function.Injective g

      Leaves ∑' (k : ℕ), (if p ∣ m + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)) = (2 : ℝ) ^ s / ((2 : ℝ) ^ p - (1 : ℝ)), with hg : Function.Injective g.

      Uses library Function.Injective A function f : α → β is called injective if f x = f y implies x = y. , Nat.eq_of_mul_eq_mul_left.

      Lean, lines 50–53
          have hg : Function.Injective g := by
      intro t t' h
      have : p * t = p * t' := by simp only [g] at h; omega
      exact Nat.eq_of_mul_eq_mul_left hp this

      targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, lines 50–53 at f1ffb04f57f2 ↗

      1. hcl.hg.this have p * t = p * t' routine: simp, omega

        Leaves t = t', with this : p * t = p * t'.

        Lean, line 52
              have : p * t = p * t' := by simp only [g] at h; omega

        targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, line 52 at f1ffb04f57f2 ↗

    8. hcl.hzero have ∀ x ∉ Set.range g, f x = (0 : ℝ)

      Leaves ∑' (k : ℕ), (if p ∣ m + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)) = (2 : ℝ) ^ s / ((2 : ℝ) ^ p - (1 : ℝ)), with hzero : ∀ x ∉ Set.range g, f x = (0 : ℝ).

      Uses library Set.range Range of a function. , if_neg, zero_div.

      Lean, lines 54–57
          have hzero : ∀ x ∉ Set.range g, f x = 0 := by
      intro x hx
      have : ¬ p ∣ m + (x + 1) := fun h => hx ((hdiv x).1 h)
      simp only [f, if_neg this, zero_div]

      targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, lines 54–57 at f1ffb04f57f2 ↗

      1. hcl.hzero.this have ¬p ∣ m + (x + (1 : ℕ))

        Leaves f x = (0 : ℝ), with this : ¬p ∣ m + (x + (1 : ℕ)).

        Lean, line 56
              have : ¬ p ∣ m + (x + 1) := fun h => hx ((hdiv x).1 h)

        targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, line 56 at f1ffb04f57f2 ↗

    9. hcl.hcomp have f ∘ g = fun (t : ℕ) => (1 / 2 : ℝ) ^ (k0 + (1 : ℕ)) * ((1 / 2 : ℝ) ^ p) ^ t

      Leaves ∑' (k : ℕ), (if p ∣ m + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)) = (2 : ℝ) ^ s / ((2 : ℝ) ^ p - (1 : ℝ)), with hcomp : f ∘ g = fun (t : ℕ) => (1 / 2 : ℝ) ^ (k0 + (1 : ℕ)) * ((1 / 2 : ℝ) ^ p) ^ t.

      Uses library Function.comp Function composition, usually written with the infix operator ∘. , if_pos, pow_mul, pow_add, one_div_pow, one_div.

      Lean, lines 58–63
          have hcomp : f ∘ g = fun t : ℕ => (1 / 2 : ℝ) ^ (k0 + 1) * ((1 / 2 : ℝ) ^ p) ^ t := by
      funext t
      have h1 : p ∣ m + (g t + 1) := (hdiv (g t)).2 ⟨t, rfl⟩
      simp only [Function.comp, f, if_pos h1, g]
      rw [← pow_mul, ← pow_add, one_div_pow, one_div]
      ring

      targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, lines 58–63 at f1ffb04f57f2 ↗

      1. hcl.hcomp.h1 have p ∣ m + (g t + (1 : ℕ))

        Leaves (f ∘ g) t = (1 / 2 : ℝ) ^ (k0 + (1 : ℕ)) * ((1 / 2 : ℝ) ^ p) ^ t, with h1 : p ∣ m + (g t + (1 : ℕ)).

        Uses library Exists.intro Existential introduction. , rfl rfl : a = a is the unique constructor of the equality type. .

        Lean, line 60
              have h1 : p ∣ m + (g t + 1) := (hdiv (g t)).2 ⟨t, rfl⟩

        targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, line 60 at f1ffb04f57f2 ↗

    10. hcl.hr0 have (0 : ℝ) ≤ (1 / 2 : ℝ) ^ p routine: positivity

      Leaves ∑' (k : ℕ), (if p ∣ m + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)) = (2 : ℝ) ^ s / ((2 : ℝ) ^ p - (1 : ℝ)), with hr0 : (0 : ℝ) ≤ (1 / 2 : ℝ) ^ p.

      Lean, line 64
          have hr0 : (0 : ℝ) ≤ (1 / 2 : ℝ) ^ p := by positivity

      targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, line 64 at f1ffb04f57f2 ↗

    11. hcl.hr1 have (1 / 2 : ℝ) ^ p < (1 : ℝ)

      Leaves ∑' (k : ℕ), (if p ∣ m + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)) = (2 : ℝ) ^ s / ((2 : ℝ) ^ p - (1 : ℝ)), with hr1 : (1 / 2 : ℝ) ^ p < (1 : ℝ).

      Uses library pow_lt_one₀.

      Lean, line 65
          have hr1 : (1 / 2 : ℝ) ^ p < 1 := pow_lt_one₀ (by norm_num) (by norm_num) hp.ne'

      targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, line 65 at f1ffb04f57f2 ↗

    12. hcl.hgeo have HasSum (fun (i : ℕ) => (1 / 2 : ℝ) ^ (k0 + (1 : ℕ)) * ((1 / 2 : ℝ) ^ p) ^ i) ((1 / 2 : ℝ) ^ (k0 + (1 : ℕ)) * ((1 : ℝ) - (1 / 2 : ℝ) ^ p)⁻¹)

      Leaves ∑' (k : ℕ), (if p ∣ m + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)) = (2 : ℝ) ^ s / ((2 : ℝ) ^ p - (1 : ℝ)), with hgeo : HasSum (fun (i : ℕ) => (1 / 2 : ℝ) ^ (k0 + (1 : ℕ)) * ((1 / 2 : ℝ) ^ p) ^ i) ((1 / 2 : ℝ) ^ (k0 + (1 : ℕ)) * ((1 : ℝ) - (1 / 2 : ℝ) ^ p)⁻¹).

      Uses library hasSum_geometric_of_lt_one.

      Lean, line 66
          have hgeo := (hasSum_geometric_of_lt_one hr0 hr1).mul_left ((1 / 2 : ℝ) ^ (k0 + 1))

      targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, line 66 at f1ffb04f57f2 ↗

    13. hcl.hH have HasSum f ((1 / 2 : ℝ) ^ (k0 + (1 : ℕ)) * ((1 : ℝ) - (1 / 2 : ℝ) ^ p)⁻¹)

      Leaves ∑' (k : ℕ), (if p ∣ m + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)) = (2 : ℝ) ^ s / ((2 : ℝ) ^ p - (1 : ℝ)), with hH : HasSum f ((1 / 2 : ℝ) ^ (k0 + (1 : ℕ)) * ((1 : ℝ) - (1 / 2 : ℝ) ^ p)⁻¹).

      Lean, line 68
          have hH := (hg.hasSum_iff hzero).1 hgeo

      targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, line 68 at f1ffb04f57f2 ↗

    14. hcl.hk have k0 + (1 : ℕ) = p - s routine: omega

      Leaves (1 / 2 : ℝ) ^ (k0 + (1 : ℕ)) * ((1 : ℝ) - (1 / 2 : ℝ) ^ p)⁻¹ = (2 : ℝ) ^ s / ((2 : ℝ) ^ p - (1 : ℝ)), with hk : k0 + (1 : ℕ) = p - s.

      Lean, line 71
          have hk : k0 + 1 = p - s := by omega

      targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, line 71 at f1ffb04f57f2 ↗

    15. hcl.h2 have (2 : ℝ) ^ p = (2 : ℝ) ^ (p - s) * (2 : ℝ) ^ s

      Leaves (1 / 2 : ℝ) ^ (p - s) * ((1 : ℝ) - (1 / 2 : ℝ) ^ p)⁻¹ = (2 : ℝ) ^ s / ((2 : ℝ) ^ p - (1 : ℝ)), with h2 : (2 : ℝ) ^ p = (2 : ℝ) ^ (p - s) * (2 : ℝ) ^ s.

      Uses library pow_add, Nat.sub_add_cancel.

      Lean, line 73
          have h2 : (2 : ℝ) ^ p = 2 ^ (p - s) * 2 ^ s := by rw [← pow_add, Nat.sub_add_cancel hsp.le]

      targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, line 73 at f1ffb04f57f2 ↗

    16. hcl.h3 have (1 : ℝ) < (2 : ℝ) ^ p

      Leaves (1 / 2 : ℝ) ^ (p - s) * ((1 : ℝ) - (1 / 2 : ℝ) ^ p)⁻¹ = (2 : ℝ) ^ s / ((2 : ℝ) ^ p - (1 : ℝ)), with h3 : (1 : ℝ) < (2 : ℝ) ^ p.

      Uses library one_lt_pow₀.

      Lean, line 74
          have h3 : (1 : ℝ) < 2 ^ p := one_lt_pow₀ (by norm_num) hp.ne'

      targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, line 74 at f1ffb04f57f2 ↗

    17. hcl.h4 have (2 : ℝ) ^ p - (1 : ℝ) ≠ (0 : ℝ) routine: linarith

      Leaves (1 / 2 : ℝ) ^ (p - s) * ((1 : ℝ) - (1 / 2 : ℝ) ^ p)⁻¹ = (2 : ℝ) ^ s / ((2 : ℝ) ^ p - (1 : ℝ)), with h4 : (2 : ℝ) ^ p - (1 : ℝ) ≠ (0 : ℝ).

      Lean, line 75
          have h4 : (2 : ℝ) ^ p - 1 ≠ 0 := by linarith

      targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, line 75 at f1ffb04f57f2 ↗

    18. hcl.h5 have (0 : ℝ) < (2 : ℝ) ^ (p - s) routine: positivity

      Leaves (1 / 2 : ℝ) ^ (p - s) * ((1 : ℝ) - (1 / 2 : ℝ) ^ p)⁻¹ = (2 : ℝ) ^ s / ((2 : ℝ) ^ p - (1 : ℝ)), with h5 : (0 : ℝ) < (2 : ℝ) ^ (p - s).

      Lean, line 76
          have h5 : (0 : ℝ) < 2 ^ (p - s) := by positivity

      targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, line 76 at f1ffb04f57f2 ↗

  2. hE0 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 ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (a * (m + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) = ∑' (k : ℕ), (↑((ω : ℕ → ℕ) (m + (k + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) + (↑((ω : ℕ → ℕ) a) : ℝ) - ∑ p ∈ a.primeFactors, (2 : ℝ) ^ (m % p) / ((2 : ℝ) ^ p - (1 : ℝ)), with hE0 : ∑' (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, Summable.tsum_finsetSum.

    Lean, lines 81–165
      have hE0 : ∑' 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
    have hω : ∀ y : ℕ, ω y = y.primeFactors.card := fun y => by
      rw [ArithmeticFunction.cardDistinctFactors_apply, Nat.primeFactors, List.card_toFinset]
    -- (a) pointwise: ω (a x) = ω x + ω a - #{p ∣ a : p ∣ x}
    have hpt : ∀ x : ℕ, x ≠ 0 → (ω (a * x) : ℝ)
        = (ω x : ℝ) + (ω a : ℝ) - ∑ p ∈ a.primeFactors, (if p ∣ x then (1 : ℝ) else 0) := by
      intro x hx
      have hint : a.primeFactors ∩ x.primeFactors = a.primeFactors.filter (· ∣ x) := 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, hx⟩
      have hc := Finset.card_union_add_card_inter a.primeFactors x.primeFactors
      rw [hint, ← Nat.primeFactors_mul ha hx] at hc
      rw [Finset.sum_boole, hω, hω, hω]
      have hc' : ((a * x).primeFactors.card : ℝ) + ((a.primeFactors.filter (· ∣ x)).card : ℝ)
          = (a.primeFactors.card : ℝ) + (x.primeFactors.card : ℝ) := by exact_mod_cast hc
      linarith
    -- (b) summability: ω y ≤ y + 1, and y ≤ B (k + 1) along both sequences
    have hle : ∀ y : ℕ, ω y ≤ y + 1 := by
      intro y
      have hsub : y.primeFactors ⊆ Finset.range (y + 1) := by
        intro p hp
        have hp' := Nat.mem_primeFactors.1 hp
        exact Finset.mem_range.2 (Nat.lt_succ_of_le (Nat.le_of_dvd (Nat.pos_of_ne_zero hp'.2.2) hp'.2.1))
      have := Finset.card_le_card hsub
      rw [Finset.card_range] at this
      rw [hω]
      omega
    have hr : ‖(1 / 2 : ℝ)‖ < 1 := by norm_num
    have hS : Summable (fun k : ℕ => ((k : ℝ) + 1) * (1 / 2 : ℝ) ^ (k + 1)) := by
      have h0 := (hasSum_coe_mul_geometric_of_norm_lt_one hr).summable
      have h1 := (summable_nat_add_iff 1).2 h0
      simpa [Nat.cast_add, Nat.cast_one] using h1
    have hsumm : ∀ (g : ℕ → ℕ) (B : ℕ), (∀ k, g k ≤ B * (k + 1)) →
        Summable (fun k : ℕ => (ω (g k) : ℝ) / 2 ^ (k + 1)) := by
      intro g B hg
      refine Summable.of_nonneg_of_le (fun k => by positivity) (fun k => ?_) (hS.mul_left ((B : ℝ) + 1))
      have h1 : ω (g k) ≤ (B + 1) * (k + 1) := by
        have := hle (g k); have := hg k; nlinarith
      have h2 : (ω (g k) : ℝ) ≤ ((B : ℝ) + 1) * ((k : ℝ) + 1) := by exact_mod_cast h1
      have hp : (0 : ℝ) < 2 ^ (k + 1) := by positivity
      rw [div_le_iff₀ hp, one_div_pow, mul_assoc, mul_assoc, one_div_mul_cancel hp.ne', mul_one]
      exact h2
    have hA : Summable (fun k : ℕ => (ω (a * (m + (k + 1))) : ℝ) / 2 ^ (k + 1)) :=
      hsumm (fun k => a * (m + (k + 1))) (a * (m + 1)) (fun k => by
        have h : m + (k + 1) ≤ (m + 1) * (k + 1) := by nlinarith
        calc a * (m + (k + 1)) ≤ a * ((m + 1) * (k + 1)) := Nat.mul_le_mul_left a h
          _ = a * (m + 1) * (k + 1) := by ring)
    have hT : Summable (fun k : ℕ => (ω (m + (k + 1)) : ℝ) / 2 ^ (k + 1)) :=
      hsumm (fun k => m + (k + 1)) (m + 1) (fun k => by nlinarith)
    have hgeo : Summable (fun k : ℕ => (1 : ℝ) / 2 ^ (k + 1)) := by
      have := (summable_geometric_two).mul_left (1 / 2 : ℝ)
      refine this.congr (fun k => ?_)
      rw [one_div_pow, pow_succ]
      field_simp
    have hI : ∀ p ∈ a.primeFactors,
        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 positivity) (fun k => ?_) hgeo
      have hp : (0 : ℝ) < 2 ^ (k + 1) := by positivity
      apply div_le_div_of_nonneg_right _ hp.le
      split_ifs <;> norm_num
    -- (c) sum the pointwise identity
    have hC : ∑' k : ℕ, (ω a : ℝ) / 2 ^ (k + 1) = (ω a : ℝ) := by
      calc ∑' k : ℕ, (ω a : ℝ) / 2 ^ (k + 1) = ∑' k : ℕ, (ω a : ℝ) / 2 / 2 ^ k :=
            tsum_congr (fun k => by rw [pow_succ, div_div, mul_comm])
        _ = (ω a : ℝ) := tsum_geometric_two' _
    have hCs : Summable (fun k : ℕ => (ω a : ℝ) / 2 ^ (k + 1)) := by
      refine (hgeo.mul_left (ω a : ℝ)).congr (fun k => ?_)
      field_simp
    have hcongr : ∀ k : ℕ, (ω (a * (m + (k + 1))) : ℝ) / 2 ^ (k + 1)
        = ((ω (m + (k + 1)) : ℝ) / 2 ^ (k + 1) + (ω a : ℝ) / 2 ^ (k + 1))
          - ∑ p ∈ a.primeFactors, (if p ∣ m + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1) := by
      intro k
      rw [hpt _ (by omega), ← Finset.sum_div]
      ring
    rw [tsum_congr hcongr, Summable.tsum_sub (hT.add hCs) (summable_sum hI),
      Summable.tsum_add hT hCs, hC, Summable.tsum_finsetSum hI]

    targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, lines 81–165 at f1ffb04f57f2 ↗

    1. hE0.h_x3c9 (hω) have ∀ (y : ℕ), (ω : ℕ → ℕ) y = y.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ω : ∀ (y : ℕ), (ω : ℕ → ℕ) y = y.primeFactors.card.

      Uses library ArithmeticFunction.cardDistinctFactors_apply, Nat.primeFactors The prime factors of a natural number as a finset. , List.card_toFinset.

      Lean, lines 85–86
          have hω : ∀ y : ℕ, ω y = y.primeFactors.card := fun y => by
      rw [ArithmeticFunction.cardDistinctFactors_apply, Nat.primeFactors, List.card_toFinset]

      targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, lines 85–86 at f1ffb04f57f2 ↗

    2. hE0.hpt have ∀ (x : ℕ), x ≠ (0 : ℕ) → (↑((ω : ℕ → ℕ) (a * x)) : ℝ) = (↑((ω : ℕ → ℕ) x) : ℝ) + (↑((ω : ℕ → ℕ) a) : ℝ) - ∑ p ∈ a.primeFactors, if p ∣ x 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 : ∀ (x : ℕ), x ≠ (0 : ℕ) → (↑((ω : ℕ → ℕ) (a * x)) : ℝ) = (↑((ω : ℕ → ℕ) x) : ℝ) + (↑((ω : ℕ → ℕ) a) : ℝ) - ∑ p ∈ a.primeFactors, if p ∣ x then (1 : ℝ) else (0 : ℝ).

      Uses library Nat.primeFactors_mul, Finset.sum_boole.

      Lean, lines 88–104
          have hpt : ∀ x : ℕ, x ≠ 0 → (ω (a * x) : ℝ)
        = (ω x : ℝ) + (ω a : ℝ) - ∑ p ∈ a.primeFactors, (if p ∣ x then (1 : ℝ) else 0) := by
      intro x hx
      have hint : a.primeFactors ∩ x.primeFactors = a.primeFactors.filter (· ∣ x) := 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, hx⟩
      have hc := Finset.card_union_add_card_inter a.primeFactors x.primeFactors
      rw [hint, ← Nat.primeFactors_mul ha hx] at hc
      rw [Finset.sum_boole, hω, hω, hω]
      have hc' : ((a * x).primeFactors.card : ℝ) + ((a.primeFactors.filter (· ∣ x)).card : ℝ)
          = (a.primeFactors.card : ℝ) + (x.primeFactors.card : ℝ) := by exact_mod_cast hc
      linarith

      targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, lines 88–104 at f1ffb04f57f2 ↗

      1. hE0.hpt.hint have a.primeFactors ∩ x.primeFactors = {x_1 ∈ a.primeFactors | x_1 ∣ x}

        Leaves (↑((ω : ℕ → ℕ) (a * x)) : ℝ) = (↑((ω : ℕ → ℕ) x) : ℝ) + (↑((ω : ℕ → ℕ) a) : ℝ) - ∑ p ∈ a.primeFactors, if p ∣ x then (1 : ℝ) else (0 : ℝ), with hint : a.primeFactors ∩ x.primeFactors = {x_1 ∈ a.primeFactors | x_1 ∣ x}.

        Uses library Finset.mem_inter, Finset.mem_filter, Nat.mem_primeFactors.

        Lean, lines 91–98
              have hint : a.primeFactors ∩ x.primeFactors = a.primeFactors.filter (· ∣ x) := 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, hx⟩

        targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, lines 91–98 at f1ffb04f57f2 ↗

        1. hE0.hpt.hint.s1 case

          Leaves (Nat.Prime p ∧ p ∣ a ∧ a ≠ (0 : ℕ)) ∧ Nat.Prime p ∧ p ∣ x ∧ x ≠ (0 : ℕ) → (Nat.Prime p ∧ p ∣ a ∧ a ≠ (0 : ℕ)) ∧ p ∣ x.

          Uses library And.intro And.intro : a → b → a ∧ b is the constructor for the And operation. .

          Lean, lines 95–96
                  · rintro ⟨h1, h2⟩
          exact ⟨h1, h2.2.1⟩

          targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, lines 95–96 at f1ffb04f57f2 ↗

        2. hE0.hpt.hint.s2 case

          Leaves (Nat.Prime p ∧ p ∣ a ∧ a ≠ (0 : ℕ)) ∧ p ∣ x → (Nat.Prime p ∧ p ∣ a ∧ a ≠ (0 : ℕ)) ∧ Nat.Prime p ∧ p ∣ x ∧ x ≠ (0 : ℕ).

          Uses library And.intro And.intro : a → b → a ∧ b is the constructor for the And operation. .

          Lean, lines 97–98
                  · rintro ⟨h1, h2⟩
          exact ⟨h1, h1.1, h2, hx⟩

          targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, lines 97–98 at f1ffb04f57f2 ↗

      2. hE0.hpt.hc have (a.primeFactors ∪ x.primeFactors).card + (a.primeFactors ∩ x.primeFactors).card = a.primeFactors.card + x.primeFactors.card

        Leaves (↑((ω : ℕ → ℕ) (a * x)) : ℝ) = (↑((ω : ℕ → ℕ) x) : ℝ) + (↑((ω : ℕ → ℕ) a) : ℝ) - ∑ p ∈ a.primeFactors, if p ∣ x then (1 : ℝ) else (0 : ℝ), with hc : (a.primeFactors ∪ x.primeFactors).card + (a.primeFactors ∩ x.primeFactors).card = a.primeFactors.card + x.primeFactors.card.

        Uses library Finset.card_union_add_card_inter.

        Lean, line 99
              have hc := Finset.card_union_add_card_inter a.primeFactors x.primeFactors

        targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, line 99 at f1ffb04f57f2 ↗

      3. hE0.hpt.hc' have (↑(a * x).primeFactors.card : ℝ) + (↑{x_1 ∈ a.primeFactors | x_1 ∣ x}.card : ℝ) = (↑a.primeFactors.card : ℝ) + (↑x.primeFactors.card : ℝ)

        Leaves (↑(a * x).primeFactors.card : ℝ) = (↑x.primeFactors.card : ℝ) + (↑a.primeFactors.card : ℝ) - (↑{x_1 ∈ a.primeFactors | x_1 ∣ x}.card : ℝ), with hc' : (↑(a * x).primeFactors.card : ℝ) + (↑{x_1 ∈ a.primeFactors | x_1 ∣ x}.card : ℝ) = (↑a.primeFactors.card : ℝ) + (↑x.primeFactors.card : ℝ).

        Lean, lines 102–103
              have hc' : ((a * x).primeFactors.card : ℝ) + ((a.primeFactors.filter (· ∣ x)).card : ℝ)
          = (a.primeFactors.card : ℝ) + (x.primeFactors.card : ℝ) := by exact_mod_cast hc

        targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, lines 102–103 at f1ffb04f57f2 ↗

    3. hE0.hle have ∀ (y : ℕ), (ω : ℕ → ℕ) y ≤ y + (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 hle : ∀ (y : ℕ), (ω : ℕ → ℕ) y ≤ y + (1 : ℕ).

      Uses library Finset.card_range.

      Lean, lines 106–115
          have hle : ∀ y : ℕ, ω y ≤ y + 1 := by
      intro y
      have hsub : y.primeFactors ⊆ Finset.range (y + 1) := by
        intro p hp
        have hp' := Nat.mem_primeFactors.1 hp
        exact Finset.mem_range.2 (Nat.lt_succ_of_le (Nat.le_of_dvd (Nat.pos_of_ne_zero hp'.2.2) hp'.2.1))
      have := Finset.card_le_card hsub
      rw [Finset.card_range] at this
      rw [hω]
      omega

      targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, lines 106–115 at f1ffb04f57f2 ↗

      1. hE0.hle.hsub have y.primeFactors ⊆ Finset.range (y + (1 : ℕ))

        Leaves (ω : ℕ → ℕ) y ≤ y + (1 : ℕ), with hsub : y.primeFactors ⊆ Finset.range (y + (1 : ℕ)).

        Uses library Finset.range range n is the set of natural numbers less than n. , Finset.mem_range, Nat.lt_succ_of_le, Nat.le_of_dvd, Nat.pos_of_ne_zero.

        Lean, lines 108–111
              have hsub : y.primeFactors ⊆ Finset.range (y + 1) := by
        intro p hp
        have hp' := Nat.mem_primeFactors.1 hp
        exact Finset.mem_range.2 (Nat.lt_succ_of_le (Nat.le_of_dvd (Nat.pos_of_ne_zero hp'.2.2) hp'.2.1))

        targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, lines 108–111 at f1ffb04f57f2 ↗

        1. hE0.hle.hsub.hp' have Nat.Prime p ∧ p ∣ y ∧ y ≠ (0 : ℕ)

          Leaves p ∈ Finset.range (y + (1 : ℕ)), with hp' : Nat.Prime p ∧ p ∣ y ∧ y ≠ (0 : ℕ).

          Uses library Nat.mem_primeFactors.

          Lean, line 110
                  have hp' := Nat.mem_primeFactors.1 hp

          targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, line 110 at f1ffb04f57f2 ↗

      2. hE0.hle.this have y.primeFactors.card ≤ (Finset.range (y + (1 : ℕ))).card

        Leaves (ω : ℕ → ℕ) y ≤ y + (1 : ℕ), with this : y.primeFactors.card ≤ (Finset.range (y + (1 : ℕ))).card.

        Uses library Finset.card_le_card.

        Lean, line 112
              have := Finset.card_le_card hsub

        targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, line 112 at f1ffb04f57f2 ↗

    4. hE0.hr have ‖(1 / 2 : ℝ)‖ < (1 : ℝ) routine: norm_num

      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 hr : ‖(1 / 2 : ℝ)‖ < (1 : ℝ).

      Lean, line 116
          have hr : ‖(1 / 2 : ℝ)‖ < 1 := by norm_num

      targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, line 116 at f1ffb04f57f2 ↗

    5. hE0.hS have Summable fun (k : ℕ) => ((↑k : ℝ) + (1 : ℝ)) * (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 hS : Summable fun (k : ℕ) => ((↑k : ℝ) + (1 : ℝ)) * (1 / 2 : ℝ) ^ (k + (1 : ℕ)).

      Uses library Summable Summable f means that f has some (infinite) sum with respect to L. , Nat.cast_add, Nat.cast_one.

      Lean, lines 117–120
          have hS : Summable (fun k : ℕ => ((k : ℝ) + 1) * (1 / 2 : ℝ) ^ (k + 1)) := by
      have h0 := (hasSum_coe_mul_geometric_of_norm_lt_one hr).summable
      have h1 := (summable_nat_add_iff 1).2 h0
      simpa [Nat.cast_add, Nat.cast_one] using h1

      targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, lines 117–120 at f1ffb04f57f2 ↗

      1. hE0.hS.h0 have Summable fun (n : ℕ) => (↑n : ℝ) * (1 / 2 : ℝ) ^ n

        Leaves Summable fun (k : ℕ) => ((↑k : ℝ) + (1 : ℝ)) * (1 / 2 : ℝ) ^ (k + (1 : ℕ)), with h0 : Summable fun (n : ℕ) => (↑n : ℝ) * (1 / 2 : ℝ) ^ n.

        Uses library hasSum_coe_mul_geometric_of_norm_lt_one If ‖r‖ < 1, then ∑' n : ℕ, n * r ^ n = r / (1 - r) ^ 2, HasSum version. .

        Lean, line 118
              have h0 := (hasSum_coe_mul_geometric_of_norm_lt_one hr).summable

        targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, line 118 at f1ffb04f57f2 ↗

      2. hE0.hS.h1 have Summable fun (n : ℕ) => (↑(n + (1 : ℕ)) : ℝ) * (1 / 2 : ℝ) ^ (n + (1 : ℕ))

        Leaves Summable fun (k : ℕ) => ((↑k : ℝ) + (1 : ℝ)) * (1 / 2 : ℝ) ^ (k + (1 : ℕ)), with h1 : Summable fun (n : ℕ) => (↑(n + (1 : ℕ)) : ℝ) * (1 / 2 : ℝ) ^ (n + (1 : ℕ)).

        Uses library summable_nat_add_iff.

        Lean, line 119
              have h1 := (summable_nat_add_iff 1).2 h0

        targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, line 119 at f1ffb04f57f2 ↗

    6. hE0.hsumm have ∀ (g : ℕ → ℕ) (B : ℕ), (∀ (k : ℕ), g k ≤ B * (k + (1 : ℕ))) → Summable fun (k : ℕ) => (↑((ω : ℕ → ℕ) (g k)) : ℝ) / (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 hsumm : ∀ (g : ℕ → ℕ) (B : ℕ), (∀ (k : ℕ), g k ≤ B * (k + (1 : ℕ))) → Summable fun (k : ℕ) => (↑((ω : ℕ → ℕ) (g k)) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)).

      Uses library Summable Summable f means that f has some (infinite) sum with respect to L. , Summable.of_nonneg_of_le Comparison test of convergence of series of non-negative real numbers. , div_le_iff₀ See div_le_iff₀' for a version with multiplication on the other side. , one_div_pow, mul_assoc, one_div_mul_cancel, mul_one.

      Lean, lines 121–130
          have hsumm : ∀ (g : ℕ → ℕ) (B : ℕ), (∀ k, g k ≤ B * (k + 1)) →
        Summable (fun k : ℕ => (ω (g k) : ℝ) / 2 ^ (k + 1)) := by
      intro g B hg
      refine Summable.of_nonneg_of_le (fun k => by positivity) (fun k => ?_) (hS.mul_left ((B : ℝ) + 1))
      have h1 : ω (g k) ≤ (B + 1) * (k + 1) := by
        have := hle (g k); have := hg k; nlinarith
      have h2 : (ω (g k) : ℝ) ≤ ((B : ℝ) + 1) * ((k : ℝ) + 1) := by exact_mod_cast h1
      have hp : (0 : ℝ) < 2 ^ (k + 1) := by positivity
      rw [div_le_iff₀ hp, one_div_pow, mul_assoc, mul_assoc, one_div_mul_cancel hp.ne', mul_one]
      exact h2

      targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, lines 121–130 at f1ffb04f57f2 ↗

      1. hE0.hsumm.h1 have (ω : ℕ → ℕ) (g k) ≤ (B + (1 : ℕ)) * (k + (1 : ℕ))

        Leaves (↑((ω : ℕ → ℕ) (g k)) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) ≤ ((↑B : ℝ) + (1 : ℝ)) * (((↑k : ℝ) + (1 : ℝ)) * (1 / 2 : ℝ) ^ (k + (1 : ℕ))), with h1 : (ω : ℕ → ℕ) (g k) ≤ (B + (1 : ℕ)) * (k + (1 : ℕ)).

        Lean, lines 125–126
              have h1 : ω (g k) ≤ (B + 1) * (k + 1) := by
        have := hle (g k); have := hg k; nlinarith

        targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, lines 125–126 at f1ffb04f57f2 ↗

        1. hE0.hsumm.h1.s1 have (ω : ℕ → ℕ) (g k) ≤ g k + (1 : ℕ)

          Leaves (ω : ℕ → ℕ) (g k) ≤ (B + (1 : ℕ)) * (k + (1 : ℕ)), with this : (ω : ℕ → ℕ) (g k) ≤ g k + (1 : ℕ).

          Lean, line 126
                  have := hle (g k); have := hg k; nlinarith

          targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, line 126 at f1ffb04f57f2 ↗

        2. hE0.hsumm.h1.s2 have g k ≤ B * (k + (1 : ℕ))

          Leaves (ω : ℕ → ℕ) (g k) ≤ (B + (1 : ℕ)) * (k + (1 : ℕ)), with this : g k ≤ B * (k + (1 : ℕ)).

          Lean, line 126
                  have := hle (g k); have := hg k; nlinarith

          targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, line 126 at f1ffb04f57f2 ↗

      2. hE0.hsumm.h2 have (↑((ω : ℕ → ℕ) (g k)) : ℝ) ≤ ((↑B : ℝ) + (1 : ℝ)) * ((↑k : ℝ) + (1 : ℝ))

        Leaves (↑((ω : ℕ → ℕ) (g k)) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) ≤ ((↑B : ℝ) + (1 : ℝ)) * (((↑k : ℝ) + (1 : ℝ)) * (1 / 2 : ℝ) ^ (k + (1 : ℕ))), with h2 : (↑((ω : ℕ → ℕ) (g k)) : ℝ) ≤ ((↑B : ℝ) + (1 : ℝ)) * ((↑k : ℝ) + (1 : ℝ)).

        Lean, line 127
              have h2 : (ω (g k) : ℝ) ≤ ((B : ℝ) + 1) * ((k : ℝ) + 1) := by exact_mod_cast h1

        targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, line 127 at f1ffb04f57f2 ↗

      3. hE0.hsumm.hp have (0 : ℝ) < (2 : ℝ) ^ (k + (1 : ℕ)) routine: positivity

        Leaves (↑((ω : ℕ → ℕ) (g k)) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) ≤ ((↑B : ℝ) + (1 : ℝ)) * (((↑k : ℝ) + (1 : ℝ)) * (1 / 2 : ℝ) ^ (k + (1 : ℕ))), with hp : (0 : ℝ) < (2 : ℝ) ^ (k + (1 : ℕ)).

        Lean, line 128
              have hp : (0 : ℝ) < 2 ^ (k + 1) := by positivity

        targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, line 128 at f1ffb04f57f2 ↗

    7. hE0.hA have Summable fun (k : ℕ) => (↑((ω : ℕ → ℕ) (a * (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 hA : Summable fun (k : ℕ) => (↑((ω : ℕ → ℕ) (a * (m + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)).

      Uses library Summable Summable f means that f has some (infinite) sum with respect to L. .

      Lean, lines 131–135
          have hA : Summable (fun k : ℕ => (ω (a * (m + (k + 1))) : ℝ) / 2 ^ (k + 1)) :=
      hsumm (fun k => a * (m + (k + 1))) (a * (m + 1)) (fun k => by
        have h : m + (k + 1) ≤ (m + 1) * (k + 1) := by nlinarith
        calc a * (m + (k + 1)) ≤ a * ((m + 1) * (k + 1)) := Nat.mul_le_mul_left a h
          _ = a * (m + 1) * (k + 1) := by ring)

      targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, lines 131–135 at f1ffb04f57f2 ↗

      1. hE0.hA.h have m + (k + (1 : ℕ)) ≤ (m + (1 : ℕ)) * (k + (1 : ℕ)) routine: nlinarith

        Leaves a * (m + (k + (1 : ℕ))) ≤ a * (m + (1 : ℕ)) * (k + (1 : ℕ)), with h : m + (k + (1 : ℕ)) ≤ (m + (1 : ℕ)) * (k + (1 : ℕ)).

        Lean, line 133
                have h : m + (k + 1) ≤ (m + 1) * (k + 1) := by nlinarith

        targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, line 133 at f1ffb04f57f2 ↗

      2. hE0.hA.s2 calc a * (m + (k + (1 : ℕ))) ≤ a * ((m + (1 : ℕ)) * (k + (1 : ℕ)))

        Closes the goal.

        Uses library Nat.mul_le_mul_left.

        Lean, line 134
                calc a * (m + (k + 1)) ≤ a * ((m + 1) * (k + 1)) := Nat.mul_le_mul_left a h

        targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, line 134 at f1ffb04f57f2 ↗

      3. hE0.hA.s3 calc routine: ring

        Closes the goal.

        Lean, line 135
                  _ = a * (m + 1) * (k + 1) := by ring)

        targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, line 135 at f1ffb04f57f2 ↗

    8. hE0.hT 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 hT : Summable fun (k : ℕ) => (↑((ω : ℕ → ℕ) (m + (k + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)).

      Uses library Summable Summable f means that f has some (infinite) sum with respect to L. .

      Lean, lines 136–137
          have hT : Summable (fun k : ℕ => (ω (m + (k + 1)) : ℝ) / 2 ^ (k + 1)) :=
      hsumm (fun k => m + (k + 1)) (m + 1) (fun k => by nlinarith)

      targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, lines 136–137 at f1ffb04f57f2 ↗

    9. hE0.hgeo 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 hgeo : Summable fun (k : ℕ) => (1 : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)).

      Uses library Summable Summable f means that f has some (infinite) sum with respect to L. , one_div_pow, pow_succ.

      Lean, lines 138–142
          have hgeo : Summable (fun k : ℕ => (1 : ℝ) / 2 ^ (k + 1)) := by
      have := (summable_geometric_two).mul_left (1 / 2 : ℝ)
      refine this.congr (fun k => ?_)
      rw [one_div_pow, pow_succ]
      field_simp

      targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, lines 138–142 at f1ffb04f57f2 ↗

      1. hE0.hgeo.this have Summable fun (i : ℕ) => (1 / 2 : ℝ) * (1 / 2 : ℝ) ^ i

        Leaves Summable fun (k : ℕ) => (1 : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)), with this : Summable fun (i : ℕ) => (1 / 2 : ℝ) * (1 / 2 : ℝ) ^ i.

        Uses library summable_geometric_two.

        Lean, line 139
              have := (summable_geometric_two).mul_left (1 / 2 : ℝ)

        targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, line 139 at f1ffb04f57f2 ↗

    10. hE0.hI have ∀ p ∈ a.primeFactors, 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 hI : ∀ p ∈ a.primeFactors, Summable fun (k : ℕ) => (if p ∣ m + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)).

      Uses library Summable Summable f means that f has some (infinite) sum with respect to L. , Summable.of_nonneg_of_le Comparison test of convergence of series of non-negative real numbers. , div_le_div_of_nonneg_right.

      Lean, lines 143–149
          have hI : ∀ p ∈ a.primeFactors,
        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 positivity) (fun k => ?_) hgeo
      have hp : (0 : ℝ) < 2 ^ (k + 1) := by positivity
      apply div_le_div_of_nonneg_right _ hp.le
      split_ifs <;> norm_num

      targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, lines 143–149 at f1ffb04f57f2 ↗

      1. hE0.hI.hp have (0 : ℝ) < (2 : ℝ) ^ (k + (1 : ℕ)) routine: positivity

        Leaves (if p ∣ m + (k + (1 : ℕ)) then (1 : ℝ) else (0 : ℝ)) / (2 : ℝ) ^ (k + (1 : ℕ)) ≤ (1 : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)), with hp : (0 : ℝ) < (2 : ℝ) ^ (k + (1 : ℕ)).

        Lean, line 147
              have hp : (0 : ℝ) < 2 ^ (k + 1) := by positivity

        targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, line 147 at f1ffb04f57f2 ↗

    11. hE0.hC have ∑' (k : ℕ), (↑((ω : ℕ → ℕ) a) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) = (↑((ω : ℕ → ℕ) a) : ℝ)

      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 hC : ∑' (k : ℕ), (↑((ω : ℕ → ℕ) a) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) = (↑((ω : ℕ → ℕ) a) : ℝ).

      Lean, lines 151–154
          have hC : ∑' k : ℕ, (ω a : ℝ) / 2 ^ (k + 1) = (ω a : ℝ) := by
      calc ∑' k : ℕ, (ω a : ℝ) / 2 ^ (k + 1) = ∑' k : ℕ, (ω a : ℝ) / 2 / 2 ^ k :=
            tsum_congr (fun k => by rw [pow_succ, div_div, mul_comm])
        _ = (ω a : ℝ) := tsum_geometric_two' _

      targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, lines 151–154 at f1ffb04f57f2 ↗

      1. hE0.hC.s1 calc ∑' (k : ℕ), (↑((ω : ℕ → ℕ) a) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) = ∑' (k : ℕ), (↑((ω : ℕ → ℕ) a) : ℝ) / (2 : ℝ) / (2 : ℝ) ^ k

        Closes the goal.

        Uses library tsum_congr, pow_succ, div_div, mul_comm.

        Lean, lines 152–153
              calc ∑' k : ℕ, (ω a : ℝ) / 2 ^ (k + 1) = ∑' k : ℕ, (ω a : ℝ) / 2 / 2 ^ k :=
            tsum_congr (fun k => by rw [pow_succ, div_div, mul_comm])

        targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, lines 152–153 at f1ffb04f57f2 ↗

      2. hE0.hC.s2 calc ∑' (k : ℕ), (↑((ω : ℕ → ℕ) a) : ℝ) / (2 : ℝ) / (2 : ℝ) ^ k = (↑((ω : ℕ → ℕ) a) : ℝ)

        Closes the goal.

        Uses library tsum_geometric_two'.

        Lean, line 154
                _ = (ω a : ℝ) := tsum_geometric_two' _

        targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, line 154 at f1ffb04f57f2 ↗

    12. hE0.hCs have Summable fun (k : ℕ) => (↑((ω : ℕ → ℕ) a) : ℝ) / (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 hCs : Summable fun (k : ℕ) => (↑((ω : ℕ → ℕ) a) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)).

      Uses library Summable Summable f means that f has some (infinite) sum with respect to L. .

      Lean, lines 155–157
          have hCs : Summable (fun k : ℕ => (ω a : ℝ) / 2 ^ (k + 1)) := by
      refine (hgeo.mul_left (ω a : ℝ)).congr (fun k => ?_)
      field_simp

      targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, lines 155–157 at f1ffb04f57f2 ↗

    13. hE0.hcongr have ∀ (k : ℕ), (↑((ω : ℕ → ℕ) (a * (m + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) = (↑((ω : ℕ → ℕ) (m + (k + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) + (↑((ω : ℕ → ℕ) a) : ℝ) / (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 hcongr : ∀ (k : ℕ), (↑((ω : ℕ → ℕ) (a * (m + (k + (1 : ℕ))))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) = (↑((ω : ℕ → ℕ) (m + (k + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (k + (1 : ℕ)) + (↑((ω : ℕ → ℕ) a) : ℝ) / (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 158–163
          have hcongr : ∀ k : ℕ, (ω (a * (m + (k + 1))) : ℝ) / 2 ^ (k + 1)
        = ((ω (m + (k + 1)) : ℝ) / 2 ^ (k + 1) + (ω a : ℝ) / 2 ^ (k + 1))
          - ∑ p ∈ a.primeFactors, (if p ∣ m + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1) := by
      intro k
      rw [hpt _ (by omega), ← Finset.sum_div]
      ring

      targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean, lines 158–163 at f1ffb04f57f2 ↗

The proof in Lean (Proof.lean)

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

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-9f8cb4ea/Proof.lean, sha256 23f61a74ecc4.
import Mathlib
import Nodes.«spec-9f8cb4ea».Context

open scoped ArithmeticFunction.omega

/-! A speculative ingredient for erdos-69 (D-29): the composite-dilation identity for the tails,
in closed form. For `a ≠ 0` and every `m`,
`∑' k, ω (a (m+k+1)) / 2^(k+1) = ∑' k, ω (m+k+1) / 2^(k+1) + ω a
  − ∑_{p ∣ a prime} 2^(m mod p) / (2^p − 1)`.
Pointwise it is `ω (a x) + #{p ∣ a : p ∣ x} = ω a + ω x` (inclusion–exclusion on prime
factors), summed against `1/2^(k+1)`; the multiples of `p` among `m+1, m+2, …` carry binary
weight exactly `2^(m mod p) / (2^p − 1)`. So a dilated tail differs from the tail itself by a
rational number with denominator dividing `∏_{p ∣ a} (2^p − 1)`: if `∑ ω(n)/2^n` were rational,
a fixed integer multiple of every dilated tail would be an integer as well. 69-C reports
(annex on erdos-69, graph PR #256) that an external formal proof of Erdős 69 rests on a
dilation identity of this kind. The identity alone proves nothing about irrationality. -/

theorem Opn.erdos_69_dilated_tail_closed :
    ∀ (a m : ℕ), a ≠ 0 →
      ∑' k : ℕ, (ω (a * (m + (k + 1))) : ℝ) / 2 ^ (k + 1)
        = ∑' k : ℕ, (ω (m + (k + 1)) : ℝ) / 2 ^ (k + 1) + (ω a : ℝ)
          - ∑ p ∈ a.primeFactors, (2 : ℝ) ^ (m % p) / (2 ^ p - 1) := by
  intro a m ha
  -- (i) the density of the multiples of p among m + 1, m + 2, … in binary weights
  have hcl : ∀ (p m : ℕ), 0 < p →
      ∑' k : ℕ, (if p ∣ m + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1)
        = 2 ^ (m % p) / (2 ^ p - 1) := by
    intro p m hp
    obtain ⟨s, hs⟩ : ∃ s, s = m % p := ⟨_, rfl⟩
    obtain ⟨Q, hQ⟩ : ∃ Q, Q = m / p := ⟨_, rfl⟩
    have hsp : s < p := hs ▸ Nat.mod_lt _ hp
    have hm : m = s + p * Q := by rw [hs, hQ]; exact (Nat.mod_add_div m p).symm
    rw [← hs]
    obtain ⟨k0, hk0⟩ : ∃ k0, k0 = p - 1 - s := ⟨_, rfl⟩
    have hdiv : ∀ k : ℕ, p ∣ m + (k + 1) ↔ ∃ t, k0 + p * t = k := by
      intro k
      constructor
      · rintro ⟨c, hc⟩
        have hcQ : Q < c := by
          have : p * Q < p * c := by omega
          exact Nat.lt_of_mul_lt_mul_left this
        obtain ⟨e, he⟩ : ∃ e, c = Q + 1 + e := ⟨c - Q - 1, by omega⟩
        refine ⟨e, ?_⟩
        rw [he, mul_add, mul_add, mul_one] at hc
        omega
      · rintro ⟨t, rfl⟩
        exact ⟨Q + 1 + t, by rw [mul_add, mul_add, mul_one]; omega⟩
    let f : ℕ → ℝ := fun k => (if p ∣ m + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1)
    let g : ℕ → ℕ := fun t => k0 + p * t
    have hg : Function.Injective g := by
      intro t t' h
      have : p * t = p * t' := by simp only [g] at h; omega
      exact Nat.eq_of_mul_eq_mul_left hp this
    have hzero : ∀ x ∉ Set.range g, f x = 0 := by
      intro x hx
      have : ¬ p ∣ m + (x + 1) := fun h => hx ((hdiv x).1 h)
      simp only [f, if_neg this, zero_div]
    have hcomp : f ∘ g = fun t : ℕ => (1 / 2 : ℝ) ^ (k0 + 1) * ((1 / 2 : ℝ) ^ p) ^ t := by
      funext t
      have h1 : p ∣ m + (g t + 1) := (hdiv (g t)).2 ⟨t, rfl⟩
      simp only [Function.comp, f, if_pos h1, g]
      rw [← pow_mul, ← pow_add, one_div_pow, one_div]
      ring
    have hr0 : (0 : ℝ) ≤ (1 / 2 : ℝ) ^ p := by positivity
    have hr1 : (1 / 2 : ℝ) ^ p < 1 := pow_lt_one₀ (by norm_num) (by norm_num) hp.ne'
    have hgeo := (hasSum_geometric_of_lt_one hr0 hr1).mul_left ((1 / 2 : ℝ) ^ (k0 + 1))
    rw [← hcomp] at hgeo
    have hH := (hg.hasSum_iff hzero).1 hgeo
    change ∑' k : ℕ, f k = _
    rw [hH.tsum_eq]
    have hk : k0 + 1 = p - s := by omega
    rw [hk]
    have h2 : (2 : ℝ) ^ p = 2 ^ (p - s) * 2 ^ s := by rw [← pow_add, Nat.sub_add_cancel hsp.le]
    have h3 : (1 : ℝ) < 2 ^ p := one_lt_pow₀ (by norm_num) hp.ne'
    have h4 : (2 : ℝ) ^ p - 1 ≠ 0 := by linarith
    have h5 : (0 : ℝ) < 2 ^ (p - s) := by positivity
    rw [one_div_pow, one_div_pow]
    field_simp
    rw [h2]
  -- (ii) the dilation identity with the densities left as sums
  have hE0 : ∑' 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
    have hω : ∀ y : ℕ, ω y = y.primeFactors.card := fun y => by
      rw [ArithmeticFunction.cardDistinctFactors_apply, Nat.primeFactors, List.card_toFinset]
    -- (a) pointwise: ω (a x) = ω x + ω a - #{p ∣ a : p ∣ x}
    have hpt : ∀ x : ℕ, x ≠ 0 → (ω (a * x) : ℝ)
        = (ω x : ℝ) + (ω a : ℝ) - ∑ p ∈ a.primeFactors, (if p ∣ x then (1 : ℝ) else 0) := by
      intro x hx
      have hint : a.primeFactors ∩ x.primeFactors = a.primeFactors.filter (· ∣ x) := 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, hx⟩
      have hc := Finset.card_union_add_card_inter a.primeFactors x.primeFactors
      rw [hint, ← Nat.primeFactors_mul ha hx] at hc
      rw [Finset.sum_boole, hω, hω, hω]
      have hc' : ((a * x).primeFactors.card : ℝ) + ((a.primeFactors.filter (· ∣ x)).card : ℝ)
          = (a.primeFactors.card : ℝ) + (x.primeFactors.card : ℝ) := by exact_mod_cast hc
      linarith
    -- (b) summability: ω y ≤ y + 1, and y ≤ B (k + 1) along both sequences
    have hle : ∀ y : ℕ, ω y ≤ y + 1 := by
      intro y
      have hsub : y.primeFactors ⊆ Finset.range (y + 1) := by
        intro p hp
        have hp' := Nat.mem_primeFactors.1 hp
        exact Finset.mem_range.2 (Nat.lt_succ_of_le (Nat.le_of_dvd (Nat.pos_of_ne_zero hp'.2.2) hp'.2.1))
      have := Finset.card_le_card hsub
      rw [Finset.card_range] at this
      rw [hω]
      omega
    have hr : ‖(1 / 2 : ℝ)‖ < 1 := by norm_num
    have hS : Summable (fun k : ℕ => ((k : ℝ) + 1) * (1 / 2 : ℝ) ^ (k + 1)) := by
      have h0 := (hasSum_coe_mul_geometric_of_norm_lt_one hr).summable
      have h1 := (summable_nat_add_iff 1).2 h0
      simpa [Nat.cast_add, Nat.cast_one] using h1
    have hsumm : ∀ (g : ℕ → ℕ) (B : ℕ), (∀ k, g k ≤ B * (k + 1)) →
        Summable (fun k : ℕ => (ω (g k) : ℝ) / 2 ^ (k + 1)) := by
      intro g B hg
      refine Summable.of_nonneg_of_le (fun k => by positivity) (fun k => ?_) (hS.mul_left ((B : ℝ) + 1))
      have h1 : ω (g k) ≤ (B + 1) * (k + 1) := by
        have := hle (g k); have := hg k; nlinarith
      have h2 : (ω (g k) : ℝ) ≤ ((B : ℝ) + 1) * ((k : ℝ) + 1) := by exact_mod_cast h1
      have hp : (0 : ℝ) < 2 ^ (k + 1) := by positivity
      rw [div_le_iff₀ hp, one_div_pow, mul_assoc, mul_assoc, one_div_mul_cancel hp.ne', mul_one]
      exact h2
    have hA : Summable (fun k : ℕ => (ω (a * (m + (k + 1))) : ℝ) / 2 ^ (k + 1)) :=
      hsumm (fun k => a * (m + (k + 1))) (a * (m + 1)) (fun k => by
        have h : m + (k + 1) ≤ (m + 1) * (k + 1) := by nlinarith
        calc a * (m + (k + 1)) ≤ a * ((m + 1) * (k + 1)) := Nat.mul_le_mul_left a h
          _ = a * (m + 1) * (k + 1) := by ring)
    have hT : Summable (fun k : ℕ => (ω (m + (k + 1)) : ℝ) / 2 ^ (k + 1)) :=
      hsumm (fun k => m + (k + 1)) (m + 1) (fun k => by nlinarith)
    have hgeo : Summable (fun k : ℕ => (1 : ℝ) / 2 ^ (k + 1)) := by
      have := (summable_geometric_two).mul_left (1 / 2 : ℝ)
      refine this.congr (fun k => ?_)
      rw [one_div_pow, pow_succ]
      field_simp
    have hI : ∀ p ∈ a.primeFactors,
        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 positivity) (fun k => ?_) hgeo
      have hp : (0 : ℝ) < 2 ^ (k + 1) := by positivity
      apply div_le_div_of_nonneg_right _ hp.le
      split_ifs <;> norm_num
    -- (c) sum the pointwise identity
    have hC : ∑' k : ℕ, (ω a : ℝ) / 2 ^ (k + 1) = (ω a : ℝ) := by
      calc ∑' k : ℕ, (ω a : ℝ) / 2 ^ (k + 1) = ∑' k : ℕ, (ω a : ℝ) / 2 / 2 ^ k :=
            tsum_congr (fun k => by rw [pow_succ, div_div, mul_comm])
        _ = (ω a : ℝ) := tsum_geometric_two' _
    have hCs : Summable (fun k : ℕ => (ω a : ℝ) / 2 ^ (k + 1)) := by
      refine (hgeo.mul_left (ω a : ℝ)).congr (fun k => ?_)
      field_simp
    have hcongr : ∀ k : ℕ, (ω (a * (m + (k + 1))) : ℝ) / 2 ^ (k + 1)
        = ((ω (m + (k + 1)) : ℝ) / 2 ^ (k + 1) + (ω a : ℝ) / 2 ^ (k + 1))
          - ∑ p ∈ a.primeFactors, (if p ∣ m + (k + 1) then (1 : ℝ) else 0) / 2 ^ (k + 1) := by
      intro k
      rw [hpt _ (by omega), ← Finset.sum_div]
      ring
    rw [tsum_congr hcongr, Summable.tsum_sub (hT.add hCs) (summable_sum hI),
      Summable.tsum_add hT hCs, hC, Summable.tsum_finsetSum hI]
  rw [hE0]
  congr 1
  exact Finset.sum_congr rfl (fun p hp => hcl p m (Nat.pos_of_mem_primeFactors hp))

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-9f8cb4ea».Context

open scoped ArithmeticFunction.omega

/-! A speculative ingredient for erdos-69 (D-29): the composite-dilation identity for the tails,
in closed form. For `a ≠ 0` and every `m`,
`∑' k, ω (a (m+k+1)) / 2^(k+1) = ∑' k, ω (m+k+1) / 2^(k+1) + ω a
  − ∑_{p ∣ a prime} 2^(m mod p) / (2^p − 1)`.
Pointwise it is `ω (a x) + #{p ∣ a : p ∣ x} = ω a + ω x` (inclusion–exclusion on prime
factors), summed against `1/2^(k+1)`; the multiples of `p` among `m+1, m+2, …` carry binary
weight exactly `2^(m mod p) / (2^p − 1)`. So a dilated tail differs from the tail itself by a
rational number with denominator dividing `∏_{p ∣ a} (2^p − 1)`: if `∑ ω(n)/2^n` were rational,
a fixed integer multiple of every dilated tail would be an integer as well. 69-C reports
(annex on erdos-69, graph PR #256) that an external formal proof of Erdős 69 rests on a
dilation identity of this kind. The identity alone proves nothing about irrationality. -/

theorem Opn.erdos_69_dilated_tail_closed :
    ∀ (a m : ℕ), a ≠ 0 →
      ∑' k : ℕ, (ω (a * (m + (k + 1))) : ℝ) / 2 ^ (k + 1)
        = ∑' k : ℕ, (ω (m + (k + 1)) : ℝ) / 2 ^ (k + 1) + (ω a : ℝ)
          - ∑ p ∈ a.primeFactors, (2 : ℝ) ^ (m % p) / (2 ^ p - 1) := by
  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 →

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

$\displaystyle \forall a,m\in\mathbb{N},\ a\ne 0:\quad \sum_{k=0}^{\infty}\frac{\omega\bigl(a(m+k+1)\bigr)}{2^{k+1}} = \sum_{k=0}^{\infty}\frac{\omega(m+k+1)}{2^{k+1}} + \omega(a) - \sum_{p\mid a}\frac{2^{\,m \bmod p}}{2^{p}-1}$

For a nonzero natural a and any natural m, the tail of ω along the multiples a(m+k+1) equals the undilated tail plus ω(a) minus, for each prime factor p of a, 2^{m mod p}/(2^p − 1), all in ℝ, with ω(n) the number of distinct prime factors of n and the last sum over a.primeFactors. Every series is Mathlib's tsum over ℝ, which is 0 when the family is not summable.

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

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

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000313.json, merge commit f1ffb04f57f2.

Verdict pass, from attestations/000313.json.

Submitter
t0929-3
Toolchain
leanprover/lean4:v4.33.1 (hash f54d0bc916bf76a7fae460ce9d078ccd1f74aeb4fd12c4b6546bca28b6aa1c63)
Mathlib
0df444a360eaa60ab8c11dca51a86af692955474
Reviewer
none needed (calibration)
StepCheckResult
1toolchainpass
2pathspass
4kernel-replaypass
5axiomspass
6hazardspass
7witnesspass
8depspass
Witness

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

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/erdos-69/nodes/spec-9f8cb4ea/Witness.lean, sha256 96f6c776b732.
import Mathlib

open scoped ArithmeticFunction.omega

theorem witness : ∃ (a m : ℕ), a ≠ 0 := ⟨1, 0, one_ne_zero⟩

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 (4)

Untrusted contributor text — the prover’s justification for a finding.

Untrusted: acknowledgment of a div-zero finding at 2 ^ (m % p) / (2 ^ p - 1)

p ranges over the prime factors of a, so p ≥ 2 and the real divisor 2^p − 1 is at least 3, never 0.

Untrusted contributor text — the prover’s justification for a finding.

Untrusted: acknowledgment of a div-zero finding at m % p

p ranges over the prime factors of a, so p ≥ 2, never 0.

Untrusted contributor text — the prover’s justification for a finding.

Untrusted: acknowledgment of a div-zero finding at ↑(ω (a * (m + (k + 1)))) / 2 ^ (k + 1)

The real divisor 2^(k+1) is positive for every k, never 0.

Untrusted contributor text — the prover’s justification for a finding.

Untrusted: acknowledgment of a div-zero finding at ↑(ω (m + (k + 1))) / 2 ^ (k + 1)

The real divisor 2^(k+1) is positive for every k, never 0.

How to read this page

How to read a statement’s page →