Open Proof Network

Problems / erdos-69 / erdos-69--h2-v2--h1-v2--h3

Logarithmic bound on the rescaled tail

erdos-69--h2-v2--h1-v2--h3

proved

Hole hbound of erdos-69--h2-v2--h1-v2 (split by 20260921T064112Z-agent-e69x-d614-partial.lean).

$\displaystyle \forall M\in\mathbb{N}:\quad \sum_{j=0}^{\infty}\frac{\omega(M+1+j)}{2^{j+1}} \le \log_{2}(M+1) + 1$

Under the hypotheses that the Lambert identity ∑_{n≥0} ω(n)/2^n = ∑_p 1/(2^p − 1) holds, that every rescaled tail splits as T(N) = ∑_{j<k} ω(N+1+j)/2^{j+1} + T(N+k)/2^k, and that every T(M) is positive, the tail T(M) is at most log₂(M+1) + 1 for every natural M, with log₂ Mathlib's Real.logb 2. Here T(M) denotes the rescaled tail ∑_{j≥0} ω(M+1+j)/2^{j+1}, a tsum over ℝ (0 if not summable), and ω(n) is the number of distinct prime factors of n.

unverified · history

Lean
theorem erdos_69__h2_v2__h1_v2__h3 : ∑' (n : ℕ), (↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n = ∑' (p : Nat.Primes), (1 : ℝ) / ((2 : ℝ) ^ (↑p : ℕ) - (1 : ℝ)) →
  (∀ (N k : ℕ),
      ∑' (j : ℕ), (↑((ω : ℕ → ℕ) (N + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) =
        ∑ j ∈ Finset.range k, (↑((ω : ℕ → ℕ) (N + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) +
          (∑' (j : ℕ), (↑((ω : ℕ → ℕ) (N + k + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ))) / (2 : ℝ) ^ k) →
    (∀ (M : ℕ), (0 : ℝ) < ∑' (j : ℕ), (↑((ω : ℕ → ℕ) (M + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ))) →
      ∀ (M : ℕ),
        ∑' (j : ℕ), (↑((ω : ℕ → ℕ) (M + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) ≤
          Real.logb (2 : ℝ) ((↑M : ℝ) + (1 : ℝ)) + (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, 000161, records the gate’s run.

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000161.json, merge commit 31ab1e7eafe4.

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. h_x3c92 (hω2) have ∀ (m : ℕ), (0 : ℕ) < m → (2 : ℕ) ^ (ω : ℕ → ℕ) m ≤ m

    Leaves ∑' (j : ℕ), (↑((ω : ℕ → ℕ) (M + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) ≤ Real.logb (2 : ℝ) ((↑M : ℝ) + (1 : ℝ)) + (1 : ℝ), with hω2 : ∀ (m : ℕ), (0 : ℕ) < m → (2 : ℕ) ^ (ω : ℕ → ℕ) m ≤ m.

    Uses library ArithmeticFunction.cardDistinctFactors_apply.

    Lean, lines 19–29
      have hω2 : ∀ m : ℕ, 0 < m → 2 ^ ω m ≤ m := by
    intro m hm
    rw [ArithmeticFunction.cardDistinctFactors_apply]
    have hprod := Nat.prod_primeFactorsList (Nat.pos_iff_ne_zero.mp hm)
    have h2 : ∀ p ∈ m.primeFactorsList, 2 ≤ p := fun p hp =>
      (Nat.prime_of_mem_primeFactorsList hp).two_le
    have hpow : 2 ^ m.primeFactorsList.length ≤ m.primeFactorsList.prod := by
      simpa using List.pow_card_le_prod _ _ h2
    calc 2 ^ m.primeFactorsList.dedup.length ≤ 2 ^ m.primeFactorsList.length :=
          Nat.pow_le_pow_right (by norm_num) (List.dedup_sublist _).length_le
      _ ≤ m := by omega

    targets/erdos-69/nodes/erdos-69--h2-v2--h1-v2--h3/Proof.lean, lines 19–29 at 31ab1e7eafe4 ↗

    1. h_x3c92.hprod have m.primeFactorsList.prod = m

      Leaves (2 : ℕ) ^ m.primeFactorsList.dedup.length ≤ m, with hprod : m.primeFactorsList.prod = m.

      Uses library Nat.prod_primeFactorsList, Nat.pos_iff_ne_zero.

      Lean, line 22
          have hprod := Nat.prod_primeFactorsList (Nat.pos_iff_ne_zero.mp hm)

      targets/erdos-69/nodes/erdos-69--h2-v2--h1-v2--h3/Proof.lean, line 22 at 31ab1e7eafe4 ↗

    2. h_x3c92.h2 have ∀ p ∈ m.primeFactorsList, (2 : ℕ) ≤ p

      Leaves (2 : ℕ) ^ m.primeFactorsList.dedup.length ≤ m, with h2 : ∀ p ∈ m.primeFactorsList, (2 : ℕ) ≤ p.

      Uses library Nat.prime_of_mem_primeFactorsList.

      Lean, lines 23–24
          have h2 : ∀ p ∈ m.primeFactorsList, 2 ≤ p := fun p hp =>
      (Nat.prime_of_mem_primeFactorsList hp).two_le

      targets/erdos-69/nodes/erdos-69--h2-v2--h1-v2--h3/Proof.lean, lines 23–24 at 31ab1e7eafe4 ↗

    3. h_x3c92.hpow have (2 : ℕ) ^ m.primeFactorsList.length ≤ m.primeFactorsList.prod

      Leaves (2 : ℕ) ^ m.primeFactorsList.dedup.length ≤ m, with hpow : (2 : ℕ) ^ m.primeFactorsList.length ≤ m.primeFactorsList.prod.

      Uses library List.pow_card_le_prod.

      Lean, lines 25–26
          have hpow : 2 ^ m.primeFactorsList.length ≤ m.primeFactorsList.prod := by
      simpa using List.pow_card_le_prod _ _ h2

      targets/erdos-69/nodes/erdos-69--h2-v2--h1-v2--h3/Proof.lean, lines 25–26 at 31ab1e7eafe4 ↗

    4. h_x3c92.s4 calc (2 : ℕ) ^ m.primeFactorsList.dedup.length ≤ (2 : ℕ) ^ m.primeFactorsList.length

      Closes the goal.

      Uses library Nat.pow_le_pow_right, List.dedup_sublist.

      Lean, lines 27–28
          calc 2 ^ m.primeFactorsList.dedup.length ≤ 2 ^ m.primeFactorsList.length :=
          Nat.pow_le_pow_right (by norm_num) (List.dedup_sublist _).length_le

      targets/erdos-69/nodes/erdos-69--h2-v2--h1-v2--h3/Proof.lean, lines 27–28 at 31ab1e7eafe4 ↗

    5. h_x3c92.s5 calc routine: omega

      Closes the goal.

      Lean, line 29
            _ ≤ m := by omega

      targets/erdos-69/nodes/erdos-69--h2-v2--h1-v2--h3/Proof.lean, line 29 at 31ab1e7eafe4 ↗

  2. h_x3c9 (hω) have ∀ (m : ℕ), (ω : ℕ → ℕ) m ≤ m

    Leaves ∑' (j : ℕ), (↑((ω : ℕ → ℕ) (M + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) ≤ Real.logb (2 : ℝ) ((↑M : ℝ) + (1 : ℝ)) + (1 : ℝ), with hω : ∀ (m : ℕ), (ω : ℕ → ℕ) m ≤ m.

    Uses library Nat.eq_zero_or_pos.

    Lean, lines 30–33
      have hω : ∀ m : ℕ, ω m ≤ m := fun m => by
    rcases Nat.eq_zero_or_pos m with rfl | hm
    · simp
    · exact le_trans (Nat.lt_two_pow_self).le (hω2 m hm)

    targets/erdos-69/nodes/erdos-69--h2-v2--h1-v2--h3/Proof.lean, lines 30–33 at 31ab1e7eafe4 ↗

    1. h_x3c9.s1 case routine: simp

      Leaves (ω : ℕ → ℕ) (0 : ℕ) ≤ (0 : ℕ).

      Lean, line 32
          · simp

      targets/erdos-69/nodes/erdos-69--h2-v2--h1-v2--h3/Proof.lean, line 32 at 31ab1e7eafe4 ↗

    2. h_x3c9.s2 case

      Leaves (ω : ℕ → ℕ) m ≤ m.

      Uses library le_trans The relation ≤ on a preorder is transitive. , Nat.lt_two_pow_self.

      Lean, line 33
          · exact le_trans (Nat.lt_two_pow_self).le (hω2 m hm)

      targets/erdos-69/nodes/erdos-69--h2-v2--h1-v2--h3/Proof.lean, line 33 at 31ab1e7eafe4 ↗

  3. hs have Summable fun (j : ℕ) => (↑((ω : ℕ → ℕ) (M + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ))

    Leaves ∑' (j : ℕ), (↑((ω : ℕ → ℕ) (M + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) ≤ Real.logb (2 : ℝ) ((↑M : ℝ) + (1 : ℝ)) + (1 : ℝ), with hs : Summable fun (j : ℕ) => (↑((ω : ℕ → ℕ) (M + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (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. .

    Lean, lines 34–46
      have hs : Summable (fun j : ℕ => (↑((ω : ℕ → ℕ) (M + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ))) := by
    have hg : Summable (fun j : ℕ => (M + 1 : ℝ) * (1 / 2 : ℝ) ^ j + (j : ℝ) ^ 1 * (1 / 2 : ℝ) ^ j) :=
      (summable_geometric_two.mul_left _).add
        (summable_pow_mul_geometric_of_norm_lt_one 1 (by norm_num))
    refine Summable.of_nonneg_of_le (fun j => by positivity) (fun j => ?_) hg
    have h1 : (ω (M + 1 + j) : ℝ) ≤ M + 1 + j := by exact_mod_cast hω _
    have hh : (1 / 2 : ℝ) ^ j * 2 ^ j = 1 := by rw [← mul_pow]; norm_num
    have e : ((M + 1 : ℝ) * (1 / 2 : ℝ) ^ j + (j : ℝ) ^ 1 * (1 / 2 : ℝ) ^ j) * 2 ^ (j + 1)
        = 2 * (M + 1 + j) := by
      rw [pow_succ]; linear_combination (2 * (M + 1 + j) : ℝ) * hh
    rw [div_le_iff₀ (by positivity), e]
    have : (0 : ℝ) ≤ M + 1 + j := by positivity
    linarith

    targets/erdos-69/nodes/erdos-69--h2-v2--h1-v2--h3/Proof.lean, lines 34–46 at 31ab1e7eafe4 ↗

    1. hs.hg have Summable fun (j : ℕ) => ((↑M : ℝ) + (1 : ℝ)) * (1 / 2 : ℝ) ^ j + (↑j : ℝ) ^ (1 : ℕ) * (1 / 2 : ℝ) ^ j

      Leaves Summable fun (j : ℕ) => (↑((ω : ℕ → ℕ) (M + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)), with hg : Summable fun (j : ℕ) => ((↑M : ℝ) + (1 : ℝ)) * (1 / 2 : ℝ) ^ j + (↑j : ℝ) ^ (1 : ℕ) * (1 / 2 : ℝ) ^ j.

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

      Lean, lines 35–37
          have hg : Summable (fun j : ℕ => (M + 1 : ℝ) * (1 / 2 : ℝ) ^ j + (j : ℝ) ^ 1 * (1 / 2 : ℝ) ^ j) :=
      (summable_geometric_two.mul_left _).add
        (summable_pow_mul_geometric_of_norm_lt_one 1 (by norm_num))

      targets/erdos-69/nodes/erdos-69--h2-v2--h1-v2--h3/Proof.lean, lines 35–37 at 31ab1e7eafe4 ↗

    2. hs.h1 have (↑((ω : ℕ → ℕ) (M + (1 : ℕ) + j)) : ℝ) ≤ (↑M : ℝ) + (1 : ℝ) + (↑j : ℝ)

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

      Lean, line 39
          have h1 : (ω (M + 1 + j) : ℝ) ≤ M + 1 + j := by exact_mod_cast hω _

      targets/erdos-69/nodes/erdos-69--h2-v2--h1-v2--h3/Proof.lean, line 39 at 31ab1e7eafe4 ↗

    3. hs.hh have (1 / 2 : ℝ) ^ j * (2 : ℝ) ^ j = (1 : ℝ)

      Leaves (↑((ω : ℕ → ℕ) (M + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) ≤ ((↑M : ℝ) + (1 : ℝ)) * (1 / 2 : ℝ) ^ j + (↑j : ℝ) ^ (1 : ℕ) * (1 / 2 : ℝ) ^ j, with hh : (1 / 2 : ℝ) ^ j * (2 : ℝ) ^ j = (1 : ℝ).

      Uses library mul_pow.

      Lean, line 40
          have hh : (1 / 2 : ℝ) ^ j * 2 ^ j = 1 := by rw [← mul_pow]; norm_num

      targets/erdos-69/nodes/erdos-69--h2-v2--h1-v2--h3/Proof.lean, line 40 at 31ab1e7eafe4 ↗

    4. hs.e have (((↑M : ℝ) + (1 : ℝ)) * (1 / 2 : ℝ) ^ j + (↑j : ℝ) ^ (1 : ℕ) * (1 / 2 : ℝ) ^ j) * (2 : ℝ) ^ (j + (1 : ℕ)) = (2 : ℝ) * ((↑M : ℝ) + (1 : ℝ) + (↑j : ℝ))

      Leaves (↑((ω : ℕ → ℕ) (M + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) ≤ ((↑M : ℝ) + (1 : ℝ)) * (1 / 2 : ℝ) ^ j + (↑j : ℝ) ^ (1 : ℕ) * (1 / 2 : ℝ) ^ j, with e : (((↑M : ℝ) + (1 : ℝ)) * (1 / 2 : ℝ) ^ j + (↑j : ℝ) ^ (1 : ℕ) * (1 / 2 : ℝ) ^ j) * (2 : ℝ) ^ (j + (1 : ℕ)) = (2 : ℝ) * ((↑M : ℝ) + (1 : ℝ) + (↑j : ℝ)).

      Uses library pow_succ.

      Lean, lines 41–43
          have e : ((M + 1 : ℝ) * (1 / 2 : ℝ) ^ j + (j : ℝ) ^ 1 * (1 / 2 : ℝ) ^ j) * 2 ^ (j + 1)
        = 2 * (M + 1 + j) := by
      rw [pow_succ]; linear_combination (2 * (M + 1 + j) : ℝ) * hh

      targets/erdos-69/nodes/erdos-69--h2-v2--h1-v2--h3/Proof.lean, lines 41–43 at 31ab1e7eafe4 ↗

    5. hs.this have (0 : ℝ) ≤ (↑M : ℝ) + (1 : ℝ) + (↑j : ℝ) routine: positivity

      Leaves (↑((ω : ℕ → ℕ) (M + (1 : ℕ) + j)) : ℝ) ≤ (2 : ℝ) * ((↑M : ℝ) + (1 : ℝ) + (↑j : ℝ)), with this : (0 : ℝ) ≤ (↑M : ℝ) + (1 : ℝ) + (↑j : ℝ).

      Lean, line 45
          have : (0 : ℝ) ≤ M + 1 + j := by positivity

      targets/erdos-69/nodes/erdos-69--h2-v2--h1-v2--h3/Proof.lean, line 45 at 31ab1e7eafe4 ↗

  4. s4 obtain ∃ (L : ℝ), L = Real.logb (2 : ℝ) ((↑M : ℝ) + (1 : ℝ))

    Leaves ∑' (j : ℕ), (↑((ω : ℕ → ℕ) (M + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) ≤ Real.logb (2 : ℝ) ((↑M : ℝ) + (1 : ℝ)) + (1 : ℝ), with L : ℝ, hL : L = Real.logb (2 : ℝ) ((↑M : ℝ) + (1 : ℝ)).

    Uses library Real.logb The real logarithm in a given base. , Exists.intro Existential introduction. , rfl rfl : a = a is the unique constructor of the equality type. .

    Lean, line 47
      obtain ⟨L, hL⟩ : ∃ L : ℝ, L = Real.logb (2 : ℝ) ((↑M : ℝ) + (1 : ℝ)) := ⟨_, rfl⟩

    targets/erdos-69/nodes/erdos-69--h2-v2--h1-v2--h3/Proof.lean, line 47 at 31ab1e7eafe4 ↗

  5. hterm have ∀ (j : ℕ), (↑((ω : ℕ → ℕ) (M + (1 : ℕ) + j)) : ℝ) ≤ L + (↑j : ℝ)

    Leaves ∑' (j : ℕ), (↑((ω : ℕ → ℕ) (M + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) ≤ L + (1 : ℝ), with hterm : ∀ (j : ℕ), (↑((ω : ℕ → ℕ) (M + (1 : ℕ) + j)) : ℝ) ≤ L + (↑j : ℝ).

    Lean, lines 49–66
      have hterm : ∀ j : ℕ, (ω (M + 1 + j) : ℝ) ≤ L + j := by
    intro j
    have hn : 2 ^ ω (M + 1 + j) ≤ (M + 1) * 2 ^ j := by
      have a := hω2 (M + 1 + j) (by omega)
      have b : j < 2 ^ j := Nat.lt_two_pow_self
      have c : 1 ≤ 2 ^ j := Nat.one_le_two_pow
      calc 2 ^ ω (M + 1 + j) ≤ M + 1 + j := a
        _ ≤ M * 2 ^ j + 2 ^ j := by
          have : M ≤ M * 2 ^ j := Nat.le_mul_of_pos_right M c
          omega
        _ = (M + 1) * 2 ^ j := by ring
    have hr : (2 : ℝ) ^ ((ω (M + 1 + j) : ℝ) - j) ≤ (M : ℝ) + 1 := by
      rw [Real.rpow_sub (by norm_num), Real.rpow_natCast, Real.rpow_natCast,
        div_le_iff₀ (by positivity)]
      exact_mod_cast hn
    have := (Real.le_logb_iff_rpow_le (by norm_num) (by positivity)).mpr hr
    rw [hL]
    linarith

    targets/erdos-69/nodes/erdos-69--h2-v2--h1-v2--h3/Proof.lean, lines 49–66 at 31ab1e7eafe4 ↗

    1. hterm.hn have (2 : ℕ) ^ (ω : ℕ → ℕ) (M + (1 : ℕ) + j) ≤ (M + (1 : ℕ)) * (2 : ℕ) ^ j

      Leaves (↑((ω : ℕ → ℕ) (M + (1 : ℕ) + j)) : ℝ) ≤ L + (↑j : ℝ), with hn : (2 : ℕ) ^ (ω : ℕ → ℕ) (M + (1 : ℕ) + j) ≤ (M + (1 : ℕ)) * (2 : ℕ) ^ j.

      Lean, lines 51–59
          have hn : 2 ^ ω (M + 1 + j) ≤ (M + 1) * 2 ^ j := by
      have a := hω2 (M + 1 + j) (by omega)
      have b : j < 2 ^ j := Nat.lt_two_pow_self
      have c : 1 ≤ 2 ^ j := Nat.one_le_two_pow
      calc 2 ^ ω (M + 1 + j) ≤ M + 1 + j := a
        _ ≤ M * 2 ^ j + 2 ^ j := by
          have : M ≤ M * 2 ^ j := Nat.le_mul_of_pos_right M c
          omega
        _ = (M + 1) * 2 ^ j := by ring

      targets/erdos-69/nodes/erdos-69--h2-v2--h1-v2--h3/Proof.lean, lines 51–59 at 31ab1e7eafe4 ↗

      1. hterm.hn.a have (2 : ℕ) ^ (ω : ℕ → ℕ) (M + (1 : ℕ) + j) ≤ M + (1 : ℕ) + j

        Leaves (2 : ℕ) ^ (ω : ℕ → ℕ) (M + (1 : ℕ) + j) ≤ (M + (1 : ℕ)) * (2 : ℕ) ^ j, with a : (2 : ℕ) ^ (ω : ℕ → ℕ) (M + (1 : ℕ) + j) ≤ M + (1 : ℕ) + j.

        Lean, line 52
              have a := hω2 (M + 1 + j) (by omega)

        targets/erdos-69/nodes/erdos-69--h2-v2--h1-v2--h3/Proof.lean, line 52 at 31ab1e7eafe4 ↗

      2. hterm.hn.b have j < (2 : ℕ) ^ j

        Leaves (2 : ℕ) ^ (ω : ℕ → ℕ) (M + (1 : ℕ) + j) ≤ (M + (1 : ℕ)) * (2 : ℕ) ^ j, with b : j < (2 : ℕ) ^ j.

        Uses library Nat.lt_two_pow_self.

        Lean, line 53
              have b : j < 2 ^ j := Nat.lt_two_pow_self

        targets/erdos-69/nodes/erdos-69--h2-v2--h1-v2--h3/Proof.lean, line 53 at 31ab1e7eafe4 ↗

      3. hterm.hn.c have (1 : ℕ) ≤ (2 : ℕ) ^ j

        Leaves (2 : ℕ) ^ (ω : ℕ → ℕ) (M + (1 : ℕ) + j) ≤ (M + (1 : ℕ)) * (2 : ℕ) ^ j, with c : (1 : ℕ) ≤ (2 : ℕ) ^ j.

        Uses library Nat.one_le_two_pow.

        Lean, line 54
              have c : 1 ≤ 2 ^ j := Nat.one_le_two_pow

        targets/erdos-69/nodes/erdos-69--h2-v2--h1-v2--h3/Proof.lean, line 54 at 31ab1e7eafe4 ↗

      4. hterm.hn.s4 calc (2 : ℕ) ^ (ω : ℕ → ℕ) (M + (1 : ℕ) + j) ≤ M + (1 : ℕ) + j

        Closes the goal.

        Lean, line 55
              calc 2 ^ ω (M + 1 + j) ≤ M + 1 + j := a

        targets/erdos-69/nodes/erdos-69--h2-v2--h1-v2--h3/Proof.lean, line 55 at 31ab1e7eafe4 ↗

      5. hterm.hn.s5 calc

        Closes the goal.

        Lean, lines 56–58
                _ ≤ M * 2 ^ j + 2 ^ j := by
          have : M ≤ M * 2 ^ j := Nat.le_mul_of_pos_right M c
          omega

        targets/erdos-69/nodes/erdos-69--h2-v2--h1-v2--h3/Proof.lean, lines 56–58 at 31ab1e7eafe4 ↗

        1. hterm.hn.s5.this have M ≤ M * (2 : ℕ) ^ j

          Leaves M + (1 : ℕ) + j ≤ M * (2 : ℕ) ^ j + (2 : ℕ) ^ j, with this : M ≤ M * (2 : ℕ) ^ j.

          Uses library Nat.le_mul_of_pos_right.

          Lean, line 57
                    have : M ≤ M * 2 ^ j := Nat.le_mul_of_pos_right M c

          targets/erdos-69/nodes/erdos-69--h2-v2--h1-v2--h3/Proof.lean, line 57 at 31ab1e7eafe4 ↗

      6. hterm.hn.s6 calc routine: ring

        Closes the goal.

        Lean, line 59
                _ = (M + 1) * 2 ^ j := by ring

        targets/erdos-69/nodes/erdos-69--h2-v2--h1-v2--h3/Proof.lean, line 59 at 31ab1e7eafe4 ↗

    2. hterm.hr have (2 : ℝ) ^ ((↑((ω : ℕ → ℕ) (M + (1 : ℕ) + j)) : ℝ) - (↑j : ℝ)) ≤ (↑M : ℝ) + (1 : ℝ)

      Leaves (↑((ω : ℕ → ℕ) (M + (1 : ℕ) + j)) : ℝ) ≤ L + (↑j : ℝ), with hr : (2 : ℝ) ^ ((↑((ω : ℕ → ℕ) (M + (1 : ℕ) + j)) : ℝ) - (↑j : ℝ)) ≤ (↑M : ℝ) + (1 : ℝ).

      Uses library Real.rpow_sub, Real.rpow_natCast, div_le_iff₀ See div_le_iff₀' for a version with multiplication on the other side. .

      Lean, lines 60–63
          have hr : (2 : ℝ) ^ ((ω (M + 1 + j) : ℝ) - j) ≤ (M : ℝ) + 1 := by
      rw [Real.rpow_sub (by norm_num), Real.rpow_natCast, Real.rpow_natCast,
        div_le_iff₀ (by positivity)]
      exact_mod_cast hn

      targets/erdos-69/nodes/erdos-69--h2-v2--h1-v2--h3/Proof.lean, lines 60–63 at 31ab1e7eafe4 ↗

    3. hterm.this have (↑((ω : ℕ → ℕ) (M + (1 : ℕ) + j)) : ℝ) - (↑j : ℝ) ≤ Real.logb (2 : ℝ) ((↑M : ℝ) + (1 : ℝ))

      Leaves (↑((ω : ℕ → ℕ) (M + (1 : ℕ) + j)) : ℝ) ≤ L + (↑j : ℝ), with this : (↑((ω : ℕ → ℕ) (M + (1 : ℕ) + j)) : ℝ) - (↑j : ℝ) ≤ Real.logb (2 : ℝ) ((↑M : ℝ) + (1 : ℝ)).

      Uses library Real.le_logb_iff_rpow_le.

      Lean, line 64
          have := (Real.le_logb_iff_rpow_le (by norm_num) (by positivity)).mpr hr

      targets/erdos-69/nodes/erdos-69--h2-v2--h1-v2--h3/Proof.lean, line 64 at 31ab1e7eafe4 ↗

  6. hg have Summable fun (j : ℕ) => L / (2 : ℝ) * (1 / 2 : ℝ) ^ j + (1 / 2 : ℝ) * ((↑j : ℝ) ^ (1 : ℕ) * (1 / 2 : ℝ) ^ j)

    Leaves ∑' (j : ℕ), (↑((ω : ℕ → ℕ) (M + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) ≤ L + (1 : ℝ), with hg : Summable fun (j : ℕ) => L / (2 : ℝ) * (1 / 2 : ℝ) ^ j + (1 / 2 : ℝ) * ((↑j : ℝ) ^ (1 : ℕ) * (1 / 2 : ℝ) ^ j).

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

    Lean, lines 67–69
      have hg : Summable (fun j : ℕ => L / 2 * (1 / 2 : ℝ) ^ j + 1 / 2 * ((j : ℝ) ^ 1 * (1 / 2 : ℝ) ^ j)) :=
    (summable_geometric_two.mul_left (L / 2)).add
      ((summable_pow_mul_geometric_of_norm_lt_one (R := ℝ) (r := 1 / 2) 1 (by norm_num)).mul_left (1 / 2))

    targets/erdos-69/nodes/erdos-69--h2-v2--h1-v2--h3/Proof.lean, lines 67–69 at 31ab1e7eafe4 ↗

  7. s7 calc ∑' (j : ℕ), (↑((ω : ℕ → ℕ) (M + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) ≤ ∑' (j : ℕ), (L / (2 : ℝ) * (1 / 2 : ℝ) ^ j + (1 / 2 : ℝ) * ((↑j : ℝ) ^ (1 : ℕ) * (1 / 2 : ℝ) ^ j))

    Closes the goal.

    Uses library Summable.tsum_le_tsum, div_le_div_of_nonneg_right.

    Lean, lines 70–76
      calc _ ≤ ∑' j : ℕ, (L / 2 * (1 / 2 : ℝ) ^ j + 1 / 2 * ((j : ℝ) ^ 1 * (1 / 2 : ℝ) ^ j)) := by
        refine Summable.tsum_le_tsum (fun j => ?_) hs hg
        have e : L / 2 * (1 / 2 : ℝ) ^ j + 1 / 2 * ((j : ℝ) ^ 1 * (1 / 2 : ℝ) ^ j)
            = (L + j) / 2 ^ (j + 1) := by
          rw [one_div_pow]; field_simp; ring
        rw [e]
        exact div_le_div_of_nonneg_right (hterm j) (by positivity)

    targets/erdos-69/nodes/erdos-69--h2-v2--h1-v2--h3/Proof.lean, lines 70–76 at 31ab1e7eafe4 ↗

    1. s7.e have L / (2 : ℝ) * (1 / 2 : ℝ) ^ j + (1 / 2 : ℝ) * ((↑j : ℝ) ^ (1 : ℕ) * (1 / 2 : ℝ) ^ j) = (L + (↑j : ℝ)) / (2 : ℝ) ^ (j + (1 : ℕ))

      Leaves (↑((ω : ℕ → ℕ) (M + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) ≤ L / (2 : ℝ) * (1 / 2 : ℝ) ^ j + (1 / 2 : ℝ) * ((↑j : ℝ) ^ (1 : ℕ) * (1 / 2 : ℝ) ^ j), with e : L / (2 : ℝ) * (1 / 2 : ℝ) ^ j + (1 / 2 : ℝ) * ((↑j : ℝ) ^ (1 : ℕ) * (1 / 2 : ℝ) ^ j) = (L + (↑j : ℝ)) / (2 : ℝ) ^ (j + (1 : ℕ)).

      Uses library one_div_pow.

      Lean, lines 72–74
              have e : L / 2 * (1 / 2 : ℝ) ^ j + 1 / 2 * ((j : ℝ) ^ 1 * (1 / 2 : ℝ) ^ j)
            = (L + j) / 2 ^ (j + 1) := by
          rw [one_div_pow]; field_simp; ring

      targets/erdos-69/nodes/erdos-69--h2-v2--h1-v2--h3/Proof.lean, lines 72–74 at 31ab1e7eafe4 ↗

  8. s8 calc

    Closes the goal.

    Uses library Summable.tsum_add, summable_geometric_two, summable_pow_mul_geometric_of_norm_lt_one, Summable.tsum_mul_left, tsum_geometric_two, pow_one, tsum_coe_mul_geometric_of_norm_lt_one If ‖r‖ < 1, then ∑' n : ℕ, n * r ^ n = r / (1 - r) ^ 2. .

    Lean, lines 77–85
        _ = L + 1 := by
        rw [Summable.tsum_add (summable_geometric_two.mul_left (L / 2))
          ((summable_pow_mul_geometric_of_norm_lt_one (R := ℝ) (r := 1 / 2) 1 (by norm_num)).mul_left (1 / 2)),
          Summable.tsum_mul_left (L / 2) summable_geometric_two,
          Summable.tsum_mul_left (1 / 2) (summable_pow_mul_geometric_of_norm_lt_one (R := ℝ) (r := 1 / 2) 1 (by norm_num)),
          tsum_geometric_two]
        simp only [pow_one]
        rw [tsum_coe_mul_geometric_of_norm_lt_one (𝕜 := ℝ) (r := 1 / 2) (by norm_num)]
        norm_num

    targets/erdos-69/nodes/erdos-69--h2-v2--h1-v2--h3/Proof.lean, lines 77–85 at 31ab1e7eafe4 ↗

The proof in Lean (Proof.lean)

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

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/erdos-69--h2-v2--h1-v2--h3/Proof.lean, sha256 886b6cfc2b95.
import Mathlib
import Nodes.«erdos-69--h2-v2--h1-v2--h3».Context

open scoped ArithmeticFunction.omega

/-! Hole `hbound` of a merged partial proof, as a node (D-12 #5, D-29).
Statement generated by the gate from the assembly; immutable (D-3). -/

theorem erdos_69__h2_v2__h1_v2__h3 : ∑' (n : ℕ), (↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n = ∑' (p : Nat.Primes), (1 : ℝ) / ((2 : ℝ) ^ (↑p : ℕ) - (1 : ℝ)) →
  (∀ (N k : ℕ),
      ∑' (j : ℕ), (↑((ω : ℕ → ℕ) (N + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) =
        ∑ j ∈ Finset.range k, (↑((ω : ℕ → ℕ) (N + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) +
          (∑' (j : ℕ), (↑((ω : ℕ → ℕ) (N + k + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ))) / (2 : ℝ) ^ k) →
    (∀ (M : ℕ), (0 : ℝ) < ∑' (j : ℕ), (↑((ω : ℕ → ℕ) (M + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ))) →
      ∀ (M : ℕ),
        ∑' (j : ℕ), (↑((ω : ℕ → ℕ) (M + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) ≤
          Real.logb (2 : ℝ) ((↑M : ℝ) + (1 : ℝ)) + (1 : ℝ) := by
  intro _ _ _ M
  have hω2 : ∀ m : ℕ, 0 < m → 2 ^ ω m ≤ m := by
    intro m hm
    rw [ArithmeticFunction.cardDistinctFactors_apply]
    have hprod := Nat.prod_primeFactorsList (Nat.pos_iff_ne_zero.mp hm)
    have h2 : ∀ p ∈ m.primeFactorsList, 2 ≤ p := fun p hp =>
      (Nat.prime_of_mem_primeFactorsList hp).two_le
    have hpow : 2 ^ m.primeFactorsList.length ≤ m.primeFactorsList.prod := by
      simpa using List.pow_card_le_prod _ _ h2
    calc 2 ^ m.primeFactorsList.dedup.length ≤ 2 ^ m.primeFactorsList.length :=
          Nat.pow_le_pow_right (by norm_num) (List.dedup_sublist _).length_le
      _ ≤ m := by omega
  have hω : ∀ m : ℕ, ω m ≤ m := fun m => by
    rcases Nat.eq_zero_or_pos m with rfl | hm
    · simp
    · exact le_trans (Nat.lt_two_pow_self).le (hω2 m hm)
  have hs : Summable (fun j : ℕ => (↑((ω : ℕ → ℕ) (M + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ))) := by
    have hg : Summable (fun j : ℕ => (M + 1 : ℝ) * (1 / 2 : ℝ) ^ j + (j : ℝ) ^ 1 * (1 / 2 : ℝ) ^ j) :=
      (summable_geometric_two.mul_left _).add
        (summable_pow_mul_geometric_of_norm_lt_one 1 (by norm_num))
    refine Summable.of_nonneg_of_le (fun j => by positivity) (fun j => ?_) hg
    have h1 : (ω (M + 1 + j) : ℝ) ≤ M + 1 + j := by exact_mod_cast hω _
    have hh : (1 / 2 : ℝ) ^ j * 2 ^ j = 1 := by rw [← mul_pow]; norm_num
    have e : ((M + 1 : ℝ) * (1 / 2 : ℝ) ^ j + (j : ℝ) ^ 1 * (1 / 2 : ℝ) ^ j) * 2 ^ (j + 1)
        = 2 * (M + 1 + j) := by
      rw [pow_succ]; linear_combination (2 * (M + 1 + j) : ℝ) * hh
    rw [div_le_iff₀ (by positivity), e]
    have : (0 : ℝ) ≤ M + 1 + j := by positivity
    linarith
  obtain ⟨L, hL⟩ : ∃ L : ℝ, L = Real.logb (2 : ℝ) ((↑M : ℝ) + (1 : ℝ)) := ⟨_, rfl⟩
  rw [← hL]
  have hterm : ∀ j : ℕ, (ω (M + 1 + j) : ℝ) ≤ L + j := by
    intro j
    have hn : 2 ^ ω (M + 1 + j) ≤ (M + 1) * 2 ^ j := by
      have a := hω2 (M + 1 + j) (by omega)
      have b : j < 2 ^ j := Nat.lt_two_pow_self
      have c : 1 ≤ 2 ^ j := Nat.one_le_two_pow
      calc 2 ^ ω (M + 1 + j) ≤ M + 1 + j := a
        _ ≤ M * 2 ^ j + 2 ^ j := by
          have : M ≤ M * 2 ^ j := Nat.le_mul_of_pos_right M c
          omega
        _ = (M + 1) * 2 ^ j := by ring
    have hr : (2 : ℝ) ^ ((ω (M + 1 + j) : ℝ) - j) ≤ (M : ℝ) + 1 := by
      rw [Real.rpow_sub (by norm_num), Real.rpow_natCast, Real.rpow_natCast,
        div_le_iff₀ (by positivity)]
      exact_mod_cast hn
    have := (Real.le_logb_iff_rpow_le (by norm_num) (by positivity)).mpr hr
    rw [hL]
    linarith
  have hg : Summable (fun j : ℕ => L / 2 * (1 / 2 : ℝ) ^ j + 1 / 2 * ((j : ℝ) ^ 1 * (1 / 2 : ℝ) ^ j)) :=
    (summable_geometric_two.mul_left (L / 2)).add
      ((summable_pow_mul_geometric_of_norm_lt_one (R := ℝ) (r := 1 / 2) 1 (by norm_num)).mul_left (1 / 2))
  calc _ ≤ ∑' j : ℕ, (L / 2 * (1 / 2 : ℝ) ^ j + 1 / 2 * ((j : ℝ) ^ 1 * (1 / 2 : ℝ) ^ j)) := by
        refine Summable.tsum_le_tsum (fun j => ?_) hs hg
        have e : L / 2 * (1 / 2 : ℝ) ^ j + 1 / 2 * ((j : ℝ) ^ 1 * (1 / 2 : ℝ) ^ j)
            = (L + j) / 2 ^ (j + 1) := by
          rw [one_div_pow]; field_simp; ring
        rw [e]
        exact div_le_div_of_nonneg_right (hterm j) (by positivity)
    _ = L + 1 := by
        rw [Summable.tsum_add (summable_geometric_two.mul_left (L / 2))
          ((summable_pow_mul_geometric_of_norm_lt_one (R := ℝ) (r := 1 / 2) 1 (by norm_num)).mul_left (1 / 2)),
          Summable.tsum_mul_left (L / 2) summable_geometric_two,
          Summable.tsum_mul_left (1 / 2) (summable_pow_mul_geometric_of_norm_lt_one (R := ℝ) (r := 1 / 2) 1 (by norm_num)),
          tsum_geometric_two]
        simp only [pow_one]
        rw [tsum_coe_mul_geometric_of_norm_lt_one (𝕜 := ℝ) (r := 1 / 2) (by norm_num)]
        norm_num
Alternate proofs (1)

Later proofs of the same statement, kept beside the first because a different proof can carry a different insight (D-25). Each passed the gate as a proof does; none changes this node's status or credit.

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.«erdos-69--h2-v2--h1-v2--h3».Context

open scoped ArithmeticFunction.omega

/-! Hole `hbound` of a merged partial proof, as a node (D-12 #5, D-29).
Statement generated by the gate from the assembly; immutable (D-3). -/

theorem erdos_69__h2_v2__h1_v2__h3 : ∑' (n : ℕ), (↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n = ∑' (p : Nat.Primes), (1 : ℝ) / ((2 : ℝ) ^ (↑p : ℕ) - (1 : ℝ)) →
  (∀ (N k : ℕ),
      ∑' (j : ℕ), (↑((ω : ℕ → ℕ) (N + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) =
        ∑ j ∈ Finset.range k, (↑((ω : ℕ → ℕ) (N + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) +
          (∑' (j : ℕ), (↑((ω : ℕ → ℕ) (N + k + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ))) / (2 : ℝ) ^ k) →
    (∀ (M : ℕ), (0 : ℝ) < ∑' (j : ℕ), (↑((ω : ℕ → ℕ) (M + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ))) →
      ∀ (M : ℕ),
        ∑' (j : ℕ), (↑((ω : ℕ → ℕ) (M + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) ≤
          Real.logb (2 : ℝ) ((↑M : ℝ) + (1 : ℝ)) + (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 M\in\mathbb{N}:\quad \sum_{j=0}^{\infty}\frac{\omega(M+1+j)}{2^{j+1}} \le \log_{2}(M+1) + 1$

Under the hypotheses that the Lambert identity ∑_{n≥0} ω(n)/2^n = ∑_p 1/(2^p − 1) holds, that every rescaled tail splits as T(N) = ∑_{j<k} ω(N+1+j)/2^{j+1} + T(N+k)/2^k, and that every T(M) is positive, the tail T(M) is at most log₂(M+1) + 1 for every natural M, with log₂ Mathlib's Real.logb 2. Here T(M) denotes the rescaled tail ∑_{j≥0} ω(M+1+j)/2^{j+1}, a tsum over ℝ (0 if not summable), and ω(n) is the number of distinct prime factors of n.

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

Rendered from targets/erdos-69/nodes/erdos-69--h2-v2--h1-v2--h3/Statement.lean. Origin: skeleton-hole.

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000161.json, merge commit 31ab1e7eafe4.

Verdict pass, from attestations/000161.json.

Submitter
t0923-69-c
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/000161.json, merge commit 31ab1e7eafe4.

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/erdos-69/nodes/erdos-69--h2-v2--h1-v2--h3/Witness.lean, sha256 26fb126cbdfb.
import Mathlib
import Nodes.«erdos-69--h2-v2--h1-v2--h3».Context

open scoped ArithmeticFunction.omega

theorem witness : ∃ M : ℕ, (∑' n : ℕ, (ω n : ℝ) / 2 ^ n = ∑' p : Nat.Primes, (1 : ℝ) / (2 ^ (p : ℕ) - 1)) ∧
    (∀ N k : ℕ,
      ∑' j : ℕ, (ω (N + 1 + j) : ℝ) / 2 ^ (j + 1)
        = ∑ j ∈ Finset.range k, (ω (N + 1 + j) : ℝ) / 2 ^ (j + 1)
          + (∑' j : ℕ, (ω (N + k + 1 + j) : ℝ) / 2 ^ (j + 1)) / 2 ^ k) ∧
    (∀ M : ℕ, 0 < ∑' j : ℕ, (ω (M + 1 + j) : ℝ) / 2 ^ (j + 1)) := by
  have h_lambert : ∑' n : ℕ, (ω n : ℝ) / 2 ^ n
      = ∑' p : Nat.Primes, (1 : ℝ) / (2 ^ (p : ℕ) - 1) := by
    -- (a) the per-prime geometric series
    have hgeom : ∀ p : ℕ, 2 ≤ p →
        ∑' k : ℕ, ((1 / 2 : ℝ) ^ p) ^ (k + 1) = 1 / (2 ^ p - 1) := by
      intro p hp
      have hr0 : (0 : ℝ) ≤ (1 / 2 : ℝ) ^ p := by positivity
      have hr1 : (1 / 2 : ℝ) ^ p < 1 := pow_lt_one₀ (by norm_num) (by norm_num) (by omega)
      have h2 : (1 : ℝ) < 2 ^ p := one_lt_pow₀ (by norm_num) (by omega)
      have h3 : (2 : ℝ) ^ p - 1 ≠ 0 := by linarith
      simp_rw [pow_succ]
      rw [tsum_mul_right, tsum_geometric_of_lt_one hr0 hr1, one_div, inv_pow]
      field_simp
    -- (D) the multiples of a prime p, reindexed
    have hD : ∀ p : ℕ, p.Prime →
        ∑' n : ℕ, (if p ∣ n + 1 then (1 / 2 : ℝ) ^ (n + 1) else 0)
          = ∑' k : ℕ, ((1 / 2 : ℝ) ^ p) ^ (k + 1) := by
      intro p hp
      have hp1 : 1 ≤ p := hp.one_lt.le
      have hk : ∀ k : ℕ, p * k + (p - 1) + 1 = p * (k + 1) := by
        intro k
        rw [Nat.mul_succ, Nat.add_assoc, Nat.sub_add_cancel hp1]
      have hg : ∀ k : ℕ, ((1 / 2 : ℝ) ^ p) ^ (k + 1) ≠ 0 := fun k => by positivity
      refine tsum_eq_tsum_of_ne_zero_bij (fun k => p * k.1 + (p - 1)) ?_ ?_ ?_
      · intro k k' h
        have h' : p * k.1 + (p - 1) = p * k'.1 + (p - 1) := h
        exact Subtype.ext (Nat.eq_of_mul_eq_mul_left hp.pos (Nat.add_right_cancel h'))
      · intro n hn
        have hn' := Function.mem_support.1 hn
        have hdvd : p ∣ n + 1 := by
          by_contra hnot
          exact hn' (if_neg hnot)
        obtain ⟨m, hm⟩ := hdvd
        rcases m with _ | k
        · omega
        · refine ⟨⟨k, hg k⟩, ?_⟩
          show p * k + (p - 1) = n
          rw [← hk k] at hm
          exact (Nat.add_right_cancel hm).symm
      · rintro ⟨k, -⟩
        show (if p ∣ p * k + (p - 1) + 1 then (1 / 2 : ℝ) ^ (p * k + (p - 1) + 1) else 0)
          = ((1 / 2 : ℝ) ^ p) ^ (k + 1)
        rw [hk k, if_pos (dvd_mul_right p (k + 1)), pow_mul]
    -- the column sums
    have hcol : ∀ p : Nat.Primes,
        ∑' n : ℕ, (if (p : ℕ) ∣ n + 1 then (1 / 2 : ℝ) ^ (n + 1) else 0)
          = 1 / (2 ^ (p : ℕ) - 1) := by
      intro p
      rw [hD p p.2, hgeom p p.2.two_le]
    -- (R) each row is summable
    have hR : ∀ p : ℕ, Summable (fun n : ℕ => if p ∣ n + 1 then (1 / 2 : ℝ) ^ (n + 1) else 0) := by
      intro p
      refine Summable.of_nonneg_of_le (fun n => ?_) (fun n => ?_)
        (summable_geometric_of_lt_one (by norm_num) (by norm_num) : Summable fun n : ℕ => (1 / 2 : ℝ) ^ n)
      · split_ifs <;> positivity
      · split_ifs
        · exact pow_le_pow_of_le_one (by norm_num) (by norm_num) (Nat.le_succ n)
        · positivity
    -- (Cb), (Sc): the column sums are summable over the primes
    have hb : ∀ p : ℕ, p.Prime → (1 : ℝ) / (2 ^ p - 1) ≤ 2 * (1 / 2 : ℝ) ^ p := by
      intro p hp
      have h2p : (2 : ℝ) ≤ 2 ^ p := by
        calc (2 : ℝ) = 2 ^ 1 := (pow_one 2).symm
          _ ≤ 2 ^ p := pow_le_pow_right₀ (by norm_num) hp.one_lt.le
      have hpos : (0 : ℝ) < 2 ^ p / 2 := by positivity
      calc (1 : ℝ) / (2 ^ p - 1) ≤ 1 / (2 ^ p / 2) := one_div_le_one_div_of_le hpos (by linarith)
        _ = 2 * (1 / 2 : ℝ) ^ p := by rw [one_div_div, one_div_pow, mul_one_div]
    have hSc : Summable (fun p : Nat.Primes => (1 : ℝ) / (2 ^ (p : ℕ) - 1)) := by
      have hg : Summable (fun n : ℕ => 2 * (1 / 2 : ℝ) ^ n) :=
        (summable_geometric_of_lt_one (by norm_num) (by norm_num)).mul_left 2
      refine Summable.of_nonneg_of_le (fun p => ?_) (fun p => ?_) (hg.subtype (fun n => n.Prime))
      · have : (1 : ℝ) < 2 ^ (p : ℕ) := one_lt_pow₀ (by norm_num) p.2.ne_zero
        exact div_nonneg zero_le_one (by linarith)
      · exact hb p p.2
    -- (C) the double family is summable
    have hC : Summable (Function.uncurry
        (fun (p : Nat.Primes) (n : ℕ) => if (p : ℕ) ∣ n + 1 then (1 / 2 : ℝ) ^ (n + 1) else 0)) := by
      have hnn : (0 : Nat.Primes × ℕ → ℝ) ≤ Function.uncurry
          (fun (p : Nat.Primes) (n : ℕ) => if (p : ℕ) ∣ n + 1 then (1 / 2 : ℝ) ^ (n + 1) else 0) := by
        rintro ⟨p, n⟩
        show (0 : ℝ) ≤ (if (p : ℕ) ∣ n + 1 then (1 / 2 : ℝ) ^ (n + 1) else 0)
        split_ifs <;> positivity
      refine (summable_prod_of_nonneg hnn).2 ⟨fun p => hR p, ?_⟩
      exact hSc.congr (fun p => (hcol p).symm)
    -- the swap
    have hswap : ∑' n : ℕ, ∑' p : Nat.Primes, (if (p : ℕ) ∣ n + 1 then (1 / 2 : ℝ) ^ (n + 1) else 0)
        = ∑' p : Nat.Primes, ∑' n : ℕ, (if (p : ℕ) ∣ n + 1 then (1 / 2 : ℝ) ^ (n + 1) else 0) :=
      hC.tsum_comm
    -- (B) the per-n collapse
    have hBgen : ∀ m : ℕ, m ≠ 0 → ∀ c : ℝ,
        ∑' p : Nat.Primes, (if (p : ℕ) ∣ m then c else 0) = (ω m : ℝ) * c := by
      intro m hm c
      let S : Finset Nat.Primes :=
        m.primeFactors.attach.map ⟨fun p => ⟨p.1, (Nat.mem_primeFactors.1 p.2).1⟩,
          fun p q h => Subtype.ext (Subtype.mk.inj h)⟩
      have hmem : ∀ p : Nat.Primes, p ∈ S ↔ (p : ℕ) ∈ m.primeFactors := by
        intro p
        constructor
        · intro hp
          obtain ⟨q, -, rfl⟩ := Finset.mem_map.1 hp
          exact q.2
        · intro hp
          exact Finset.mem_map.2 ⟨⟨p.1, hp⟩, Finset.mem_attach _ _, Subtype.ext rfl⟩
      have hfin : ∀ p : Nat.Primes, p ∉ S → (if (p : ℕ) ∣ m then c else 0) = 0 := by
        intro p hp
        rw [if_neg]
        intro hdvd
        exact hp ((hmem p).2 (Nat.mem_primeFactors.2 ⟨p.2, hdvd, hm⟩))
      rw [tsum_eq_sum hfin]
      rw [Finset.sum_ite_of_true (fun p hp => (Nat.mem_primeFactors.1 ((hmem p).1 hp)).2.1)]
      rw [Finset.sum_const, nsmul_eq_mul]
      have hcard : S.card = m.primeFactors.card := by
        simp [S, Finset.card_map, Finset.card_attach]
      have hω : (m.primeFactors.card : ℝ) = ω m := by
        simp [ArithmeticFunction.cardDistinctFactors_apply]
        rfl
      rw [hcard, hω]
    have hB : ∀ n : ℕ,
        ∑' p : Nat.Primes, (if (p : ℕ) ∣ n + 1 then (1 / 2 : ℝ) ^ (n + 1) else 0)
          = (ω (n + 1) : ℝ) / 2 ^ (n + 1) := by
      intro n
      rw [hBgen (n + 1) n.succ_ne_zero, one_div_pow, mul_one_div]
    -- the original series is summable (as in the partial)
    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))
    -- assembly
    calc ∑' n : ℕ, (ω n : ℝ) / 2 ^ n
        = ∑' n : ℕ, (ω (n + 1) : ℝ) / 2 ^ (n + 1) := by
          rw [hsum.tsum_eq_zero_add]
          simp
      _ = ∑' n : ℕ, ∑' p : Nat.Primes, (if (p : ℕ) ∣ n + 1 then (1 / 2 : ℝ) ^ (n + 1) else 0) :=
          tsum_congr (fun n => (hB n).symm)
      _ = ∑' p : Nat.Primes, ∑' n : ℕ, (if (p : ℕ) ∣ n + 1 then (1 / 2 : ℝ) ^ (n + 1) else 0) := hswap
      _ = ∑' p : Nat.Primes, (1 : ℝ) / (2 ^ (p : ℕ) - 1) := tsum_congr hcol
  have omega_series_summable : Summable (fun n : ℕ => (ω n : ℝ) / 2 ^ n) := by
    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]
    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 tail_summable : ∀ (N : ℕ), Summable (fun j : ℕ => (ω (N + 1 + j) : ℝ) / 2 ^ (j + 1)) := by
    intro N
    have hshift : Summable (fun j : ℕ => (ω (j + (N + 1)) : ℝ) / 2 ^ (j + (N + 1))) :=
      (summable_nat_add_iff (f := fun n : ℕ => (ω n : ℝ) / 2 ^ n) (N + 1)).2 omega_series_summable
    refine (hshift.mul_left ((2 : ℝ) ^ N)).congr (fun j => ?_)
    rw [show j + (N + 1) = N + 1 + j by omega]
    rw [show (2 : ℝ) ^ (N + 1 + j) = 2 ^ N * 2 ^ (j + 1) by rw [← pow_add]; congr 1; omega]
    field_simp
  have hpos : ∀ M : ℕ, 0 < ∑' j : ℕ, (ω (M + 1 + j) : ℝ) / 2 ^ (j + 1) := by
    intro M
    refine (tail_summable M).tsum_pos (fun j => by positivity) 1 ?_
    have h1 : 0 < ω (M + 1 + 1) := by
      rw [ArithmeticFunction.cardDistinctFactors_apply]
      have : (M + 1 + 1).primeFactors.Nonempty := Nat.nonempty_primeFactors.2 (by omega)
      exact Finset.card_pos.2 this
    have : (0 : ℝ) < (ω (M + 1 + 1) : ℝ) := by exact_mod_cast h1
    positivity
  have tail_step : ∀ (N : ℕ), ∑' j : ℕ, (ω (N + 1 + j) : ℝ) / 2 ^ (j + 1)
      = (ω (N + 1) : ℝ) / 2 + (∑' j : ℕ, (ω (N + 1 + 1 + j) : ℝ) / 2 ^ (j + 1)) / 2 := by
    intro N
    rw [(tail_summable N).tsum_eq_zero_add, ← tsum_div_const]
    congr 1
    · simp
    · refine tsum_congr (fun j => ?_)
      rw [show N + 1 + (j + 1) = N + 1 + 1 + j by omega, pow_succ (2 : ℝ) (j + 1)]
      field_simp
  have hsplit : ∀ N k : ℕ,
    ∑' j : ℕ, (ω (N + 1 + j) : ℝ) / 2 ^ (j + 1)
      = ∑ j ∈ Finset.range k, (ω (N + 1 + j) : ℝ) / 2 ^ (j + 1)
        + (∑' j : ℕ, (ω (N + k + 1 + j) : ℝ) / 2 ^ (j + 1)) / 2 ^ k := by
    intro N k
    induction k with
    | zero => simp
    | succ k ih =>
      rw [ih, tail_step (N + k), Finset.sum_range_succ]
      rw [show N + (k + 1) = N + k + 1 by omega, show N + 1 + k = N + k + 1 by omega, pow_succ]
      field_simp
      ring
  have omega_le_logb : ∀ (n : ℕ), ∀ (hn : 1 ≤ n), (ω n : ℝ) ≤ Real.logb 2 n := by
    intro n hn
    have h1 : 2 ^ ω n ≤ n := by
      rw [ArithmeticFunction.cardDistinctFactors_apply]
      calc 2 ^ n.primeFactorsList.dedup.length = 2 ^ n.primeFactors.card := rfl
        _ ≤ ∏ p ∈ n.primeFactors, p :=
            Finset.pow_card_le_prod _ _ _ (fun p hp => (Nat.prime_of_mem_primeFactors hp).two_le)
        _ ≤ n := Nat.le_of_dvd (by omega) (Nat.prod_primeFactors_dvd n)
    have h2 : ((2 : ℝ) ^ ω n) ≤ (n : ℝ) := by exact_mod_cast h1
    have hn0 : (0 : ℝ) < n := by exact_mod_cast hn
    rw [Real.le_logb_iff_rpow_le (by norm_num) hn0, Real.rpow_natCast]
    exact h2
  have geo1 : HasSum (fun j : ℕ => (1 : ℝ) / 2 ^ (j + 1)) 1 := by
    have h' := (hasSum_geometric_two).mul_left (1 / 2 : ℝ)
    have hf : (fun j : ℕ => (1 : ℝ) / 2 ^ (j + 1)) = fun i : ℕ => 1 / 2 * (1 / 2 : ℝ) ^ i := by
      funext j
      rw [pow_succ, one_div_pow]
      field_simp
    have hv : (1 / 2 * 2 : ℝ) = 1 := by norm_num
    rw [hv] at h'
    rw [hf]
    exact h'
  have geo2 : HasSum (fun j : ℕ => (j : ℝ) / 2 ^ (j + 1)) 1 := by
    have h' := (hasSum_coe_mul_geometric_of_norm_lt_one (r := (1 / 2 : ℝ))
      (by norm_num [Real.norm_eq_abs])).mul_left (1 / 2 : ℝ)
    have hf : (fun j : ℕ => (j : ℝ) / 2 ^ (j + 1)) = fun i : ℕ => 1 / 2 * ((i : ℝ) * (1 / 2 : ℝ) ^ i) := by
      funext j
      rw [pow_succ, one_div_pow]
      field_simp
    have hv : (1 / 2 * (1 / 2 / (1 - 1 / 2) ^ 2) : ℝ) = 1 := by norm_num
    rw [hv] at h'
    rw [hf]
    exact h'
  have hbound : ∀ M : ℕ,
    ∑' j : ℕ, (ω (M + 1 + j) : ℝ) / 2 ^ (j + 1) ≤ Real.logb 2 ((M : ℝ) + 1) + 1 := by
    intro M
    have hL : 0 ≤ Real.logb 2 ((M : ℝ) + 1) := Real.logb_nonneg (by norm_num) (by linarith [Nat.cast_nonneg (α := ℝ) M])
    have hterm : ∀ j : ℕ, (ω (M + 1 + j) : ℝ) / 2 ^ (j + 1)
        ≤ Real.logb 2 ((M : ℝ) + 1) * (1 / 2 ^ (j + 1)) + (j : ℝ) / 2 ^ (j + 1) := by
      intro j
      have h1 := omega_le_logb (M + 1 + j) (by omega)
      have hM : (0 : ℝ) < (M : ℝ) + 1 := by positivity
      have hj : (0 : ℝ) < (j : ℝ) + 1 := by positivity
      have h2 : Real.logb 2 ((M + 1 + j : ℕ) : ℝ) ≤ Real.logb 2 (((M : ℝ) + 1) * ((j : ℝ) + 1)) := by
        apply Real.logb_le_logb_of_le (by norm_num) (by positivity)
        push_cast
        nlinarith [Nat.cast_nonneg (α := ℝ) M, Nat.cast_nonneg (α := ℝ) j]
      rw [Real.logb_mul hM.ne' hj.ne'] at h2
      have h3 : Real.logb 2 ((j : ℝ) + 1) ≤ (j : ℝ) := by
        rw [Real.logb_le_iff_le_rpow (by norm_num) hj, Real.rpow_natCast]
        have : j + 1 ≤ 2 ^ j := Nat.lt_two_pow_self
        exact_mod_cast this
      have hp : (0 : ℝ) < 2 ^ (j + 1) := by positivity
      rw [mul_one_div, ← add_div]
      exact div_le_div_of_nonneg_right (by linarith) hp.le
    have hs : HasSum (fun j : ℕ => Real.logb 2 ((M : ℝ) + 1) * (1 / 2 ^ (j + 1)) + (j : ℝ) / 2 ^ (j + 1))
        (Real.logb 2 ((M : ℝ) + 1) * 1 + 1) := (geo1.mul_left _).add geo2
    calc ∑' j : ℕ, (ω (M + 1 + j) : ℝ) / 2 ^ (j + 1)
        ≤ ∑' j : ℕ, (Real.logb 2 ((M : ℝ) + 1) * (1 / 2 ^ (j + 1)) + (j : ℝ) / 2 ^ (j + 1)) :=
          (tail_summable M).tsum_le_tsum hterm hs.summable
      _ = Real.logb 2 ((M : ℝ) + 1) + 1 := by rw [hs.tsum_eq, mul_one]
  exact ⟨0, h_lambert, hsplit, hpos⟩

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 →

How to read this page

How to read a statement’s page →