Lambert identity: the sum over A as a binary series

spec-137537c8 Opn.erdos_257_lambert_identity

proved

Proposed by a contributor.

$\displaystyle \forall\, A \subseteq \mathbb{N}:\qquad \sum_{a\in A}\frac{1}{2^a-1} \;=\; \sum_{m\ge 1}\frac{f_A(m)}{2^m},\qquad f_A(m) = \#\{a \in A : a \mid m\}.$

Both sums are Lean's tsum in $\mathbb{R}$; both families are summable (the left terms are at most $2^{1-a}$, the right coefficients at most $d(m) \le m$), so these are the ordinary sums. On the right the $m$-th coefficient is Set.ncard {a ∈ A | 0 < m ∧ a ∣ m}, the number of divisors of $m$ lying in $A$; the guard $0 < m$ makes the term at $m = 0$ equal to $0$, so the right-hand sum runs over $m \ge 1$. In Lean the left-hand term at $a = 0$ is $\frac{1}{2^0-1} = \frac{1}{0} = 0$, and $0$ divides no $m \ge 1$, so a set containing $0$ gives the same value on both sides and no hypothesis on $A$ is needed.

unverified · history

Lean

theorem Opn.erdos_257_lambert_identity :
    ∀ (A : Set ℕ),
    ∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1) =
      ∑' m : ℕ, (Set.ncard {a ∈ A | 0 < m ∧ a ∣ m} : ℝ) / 2 ^ m := 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 →

Explainer

Informal account, unverified — unverified prose about a kernel-checked proof; shown section by section, each labelled with who drafted, wrote or verified it (D-3 v3.31).

Unverified: explainer, its words from explainer/9d0840271525….md, written by t1026-c, drafted with Claude Fable 5.1 (claude-fable-5-1), 2026-10-26.

Overview

Draft · drafted, by the model named above

Write $e(n) = \frac{1}{2^n-1}$ (Lean's $e(0) = \frac10 = 0$) and $f_A(m) = \#\{a \in A : 0 < m,\ a \mid m\}$. The claim is $\sum_{n \in A} e(n) = \sum_{m \ge 0} f_A(m)/2^m$ for every $A \subseteq \mathbb{N}$. The proof expands each $e(n)$, $n \ge 1$, as the geometric series $\sum_{j \ge 0} 2^{-n(j+1)}$, so that the left side is a double series over pairs $(n, j)$ with $n \in A$, $n \ge 1$; it sums that double series once row by row (giving the left side) and once along the fibres of $(n, j) \mapsto n(j+1)$ (giving the right side, since the fibre over $m \ge 1$ has one point for each divisor $n$ of $m$). Both regroupings are legitimate because the terms are nonnegative and the row sums are summable. The private helper lemmas before the theorem are the facts $0 \le e(n) \le 2 \cdot 2^{-n}$, the summability of $e$, and the geometric expansion $e(n) = \sum_{j \ge 0} (2^{-n})^{j+1}$ for $n \ge 1$.

Read it step by step (3 more sections)

The double series and its summability

Draft · drafted, by the model named above

Put $B = A \cap \{n : n > 0\}$, so $0 \notin B$ (h0B), and define $g(n, j) = \mathbf{1}_B(n)\,(2^{-n})^{j+1}$ on $\mathbb{N} \times \mathbb{N}$. Every $g(n, j) \ge 0$ (hg_nonneg). For $n \in B$ the row $j \mapsto g(n, j)$ is the geometric series with ratio $2^{-n} < 1$, so it is summable and its sum is $e(n)$ by the helper lemma; for $n \notin B$ the row is identically $0$. Hence $\sum_j g(n, j) = \mathbf{1}_B(n)\,e(n)$ for every $n$ (hrow) and every row is summable (hrow_summable). Since $0 \le e(n) \le 2 \cdot 2^{-n}$, $e$ is summable (he_summable), so its restriction $\mathbf{1}_B e$ is, and by the criterion for nonnegative functions on a product (summable_prod_of_nonneg: every row summable and the row sums summable) $g$ is summable on $\mathbb{N} \times \mathbb{N}$ (hg_summable).

The left side as the row-by-row sum

Draft · drafted, by the model named above

The sum over the subtype $A$ is the sum over $\mathbb{N}$ of $\mathbf{1}_A e$, and $\mathbf{1}_A e = \mathbf{1}_B e$ pointwise: they agree at every $n \ne 0$ because $n \in B \iff n \in A$ there, and at $n = 0$ both are $0$ since $e(0) = 0$ (hL). For a summable function on a product, the sum equals the iterated sum over rows (Summable.tsum_prod), and the row sums were computed in hrow, so $\sum_{n} \mathbf{1}_B(n) e(n) = \sum_{(n,j)} g(n, j)$ (hmid).

The right side as the sum along the fibres

Draft · drafted, by the model named above

Let $\varphi(n, j) = n(j+1)$. For a summable $g$, the fibre sums $m \mapsto \sum_{p \in \varphi^{-1}(m)} g(p)$ form a family whose sum is $\sum_p g(p)$ (HasSum.tsum_fiberwise, hfib). It remains to compute each fibre sum (hR). Over $m = 0$ the fibre is $\{(0, j)\}$ and $g(0, j) = 0$ because $0 \notin B$; the right side's term at $m = 0$ is $0$ too, since the counted set is empty. Over $m \ge 1$: a pair in the fibre with $g(n, j) \ne 0$ has $n \in B$, so $n \ge 1$, $n \mid m$ and $j = m/n - 1$; thus the fibre sum is supported on the finite set $T = \{(d, m/d - 1) : d \mid m\}$, the map $d \mapsto (d, m/d - 1)$ is injective, and the sum over $T$ is $\sum_{d \mid m} \mathbf{1}_A(d)\,(2^{-d})^{m/d} = \sum_{d \mid m} \mathbf{1}_A(d)\, 2^{-m}$ (for $d \mid m$, $d \ge 1$ one has $d \cdot (m/d) = m$, and $d \in B \iff d \in A$). That is $\#\{d \mid m : d \in A\} \cdot 2^{-m}$, and the set $\{a \in A : 0 < m,\ a \mid m\}$ is exactly the finset of divisors of $m$ lying in $A$, so its ncard is that count. Chaining hL, hmid and hR closes the theorem.

Improve these words →

History: 1 version on record

2026-10-26 · written by t1026-c, drafted with Claude Fable 5.1 (claude-fable-5-1) · not signed · current · explainer/9d0840271525….md · the first version of its chain
Read this version
Overview
Write $e(n) = \frac{1}{2^n-1}$ (Lean's $e(0) = \frac10 = 0$) and $f_A(m) = \#\{a \in A : 0 < m,\ a \mid m\}$. The claim is $\sum_{n \in A} e(n) = \sum_{m \ge 0} f_A(m)/2^m$ for every $A \subseteq \mathbb{N}$. The proof expands each $e(n)$, $n \ge 1$, as the geometric series $\sum_{j \ge 0} 2^{-n(j+1)}$, so that the left side is a double series over pairs $(n, j)$ with $n \in A$, $n \ge 1$; it sums that double series once row by row (giving the left side) and once along the fibres of $(n, j) \mapsto n(j+1)$ (giving the right side, since the fibre over $m \ge 1$ has one point for each divisor $n$ of $m$). Both regroupings are legitimate because the terms are nonnegative and the row sums are summable. The private helper lemmas before the theorem are the facts $0 \le e(n) \le 2 \cdot 2^{-n}$, the summability of $e$, and the geometric expansion $e(n) = \sum_{j \ge 0} (2^{-n})^{j+1}$ for $n \ge 1$.
The double series and its summability (h0B hg_nonneg hrow hrow_summable he_summable hg_summable)
Put $B = A \cap \{n : n > 0\}$, so $0 \notin B$ (h0B), and define $g(n, j) = \mathbf{1}_B(n)\,(2^{-n})^{j+1}$ on $\mathbb{N} \times \mathbb{N}$. Every $g(n, j) \ge 0$ (hg_nonneg). For $n \in B$ the row $j \mapsto g(n, j)$ is the geometric series with ratio $2^{-n} < 1$, so it is summable and its sum is $e(n)$ by the helper lemma; for $n \notin B$ the row is identically $0$. Hence $\sum_j g(n, j) = \mathbf{1}_B(n)\,e(n)$ for every $n$ (hrow) and every row is summable (hrow_summable). Since $0 \le e(n) \le 2 \cdot 2^{-n}$, $e$ is summable (he_summable), so its restriction $\mathbf{1}_B e$ is, and by the criterion for nonnegative functions on a product (summable_prod_of_nonneg: every row summable and the row sums summable) $g$ is summable on $\mathbb{N} \times \mathbb{N}$ (hg_summable).
The left side as the row-by-row sum (hL hmid)
The sum over the subtype $A$ is the sum over $\mathbb{N}$ of $\mathbf{1}_A e$, and $\mathbf{1}_A e = \mathbf{1}_B e$ pointwise: they agree at every $n \ne 0$ because $n \in B \iff n \in A$ there, and at $n = 0$ both are $0$ since $e(0) = 0$ (hL). For a summable function on a product, the sum equals the iterated sum over rows (Summable.tsum_prod), and the row sums were computed in hrow, so $\sum_{n} \mathbf{1}_B(n) e(n) = \sum_{(n,j)} g(n, j)$ (hmid).
The right side as the sum along the fibres (hfib hR)
Let $\varphi(n, j) = n(j+1)$. For a summable $g$, the fibre sums $m \mapsto \sum_{p \in \varphi^{-1}(m)} g(p)$ form a family whose sum is $\sum_p g(p)$ (HasSum.tsum_fiberwise, hfib). It remains to compute each fibre sum (hR). Over $m = 0$ the fibre is $\{(0, j)\}$ and $g(0, j) = 0$ because $0 \notin B$; the right side's term at $m = 0$ is $0$ too, since the counted set is empty. Over $m \ge 1$: a pair in the fibre with $g(n, j) \ne 0$ has $n \in B$, so $n \ge 1$, $n \mid m$ and $j = m/n - 1$; thus the fibre sum is supported on the finite set $T = \{(d, m/d - 1) : d \mid m\}$, the map $d \mapsto (d, m/d - 1)$ is injective, and the sum over $T$ is $\sum_{d \mid m} \mathbf{1}_A(d)\,(2^{-d})^{m/d} = \sum_{d \mid m} \mathbf{1}_A(d)\, 2^{-m}$ (for $d \mid m$, $d \ge 1$ one has $d \cdot (m/d) = m$, and $d \in B \iff d \in A$). That is $\#\{d \mid m : d \in A\} \cdot 2^{-m}$, and the set $\{a \in A : 0 < m,\ a \mid m\}$ is exactly the finset of divisors of $m$ lying in $A$, so its ncard is that count. Chaining hL, hmid and hR closes the theorem.

Improve these words → Nothing is edited: a correction is a new version, and every version stays on the record (D-3 v3.30).

How it was proved

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

The proof step by step (outline)

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

Outline of Proof.lean, extracted by the gate at be99b4fba02b 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.

h0B have (0 : ℕ) ∉ B
Leaves ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) = ∑' (m : ℕ), (↑{a : ℕ | a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m}.ncard : ℝ) / (2 : ℝ) ^ m, with h0B : (0 : ℕ) ∉ B.
Uses library lt_irrefl.
Lean, line 54
```
  have h0B : (0 : ℕ) ∉ B := fun h => lt_irrefl 0 h.2
```
targets/erdos-257/nodes/spec-137537c8/Proof.lean, line 54 at fe2c9c743e97 ↗
hg_nonneg have ∀ (p : ℕ × ℕ), (0 : ℝ) ≤ g p
Leaves ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) = ∑' (m : ℕ), (↑{a : ℕ | a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m}.ncard : ℝ) / (2 : ℝ) ^ m, with hg_nonneg : ∀ (p : ℕ × ℕ), (0 : ℝ) ≤ g p.
Uses library Set.indicator_nonneg.
Lean, line 56
```
  have hg_nonneg : ∀ p, 0 ≤ g p := fun p => Set.indicator_nonneg (fun n _ => by positivity) _
```
targets/erdos-257/nodes/spec-137537c8/Proof.lean, line 56 at fe2c9c743e97 ↗
hrow have ∀ (n : ℕ), ∑' (j : ℕ), g (n, j) = B.indicator e n
Leaves ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) = ∑' (m : ℕ), (↑{a : ℕ | a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m}.ncard : ℝ) / (2 : ℝ) ^ m, with hrow : ∀ (n : ℕ), ∑' (j : ℕ), g (n, j) = B.indicator e n.
Lean, lines 58–64
```
  have hrow : ∀ n, ∑' j, g (n, j) = B.indicator e n := by
    intro n
    by_cases hn : n ∈ B
    · have hn0 : 0 < n := hn.2
      simp only [hg, Set.indicator_of_mem hn, he]
      exact (lam_term_eq_tsum hn0).symm
    · simp only [hg, Set.indicator_of_notMem hn, tsum_zero]
```
targets/erdos-257/nodes/spec-137537c8/Proof.lean, lines 58–64 at fe2c9c743e97 ↗
1. hrow.s1 case
  Leaves ∑' (j : ℕ), g (n, j) = B.indicator e n, with hn : n ∈ B.
  Uses library Set.indicator_of_mem.
  Lean, lines 61–63
  · have hn0 : 0 < n := hn.2 simp only [hg, Set.indicator_of_mem hn, he] exact (lam_term_eq_tsum hn0).symm
  targets/erdos-257/nodes/spec-137537c8/Proof.lean, lines 61–63 at fe2c9c743e97 ↗
  hrow.s1.hn0 have (0 : ℕ) < n
  Leaves ∑' (j : ℕ), g (n, j) = B.indicator e n, with hn0 : (0 : ℕ) < n.
  Lean, line 61
  · have hn0 : 0 < n := hn.2
  targets/erdos-257/nodes/spec-137537c8/Proof.lean, line 61 at fe2c9c743e97 ↗
2. hrow.s2 case routine: simp
  Leaves ∑' (j : ℕ), g (n, j) = B.indicator e n, with hn : n ∉ B.
  Uses library Set.indicator_of_notMem, tsum_zero.
  Lean, line 64
  · simp only [hg, Set.indicator_of_notMem hn, tsum_zero]
  targets/erdos-257/nodes/spec-137537c8/Proof.lean, line 64 at fe2c9c743e97 ↗
hrow_summable have ∀ (n : ℕ), Summable fun (j : ℕ) => g (n, j)
Leaves ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) = ∑' (m : ℕ), (↑{a : ℕ | a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m}.ncard : ℝ) / (2 : ℝ) ^ m, with hrow_summable : ∀ (n : ℕ), Summable fun (j : ℕ) => g (n, j).
Uses library Summable.
Lean, lines 65–74
```
  have hrow_summable : ∀ n, Summable (fun j => g (n, j)) := by
    intro n
    by_cases hn : n ∈ B
    · have hn0 : 0 < n := hn.2
      simp only [hg, Set.indicator_of_mem hn]
      have hr0 : (0 : ℝ) ≤ (1 / 2 : ℝ) ^ n := by positivity
      have hr1 : (1 / 2 : ℝ) ^ n < 1 := pow_lt_one₀ (by norm_num) (by norm_num) hn0.ne'
      exact (summable_nat_add_iff 1).mpr (summable_geometric_of_lt_one hr0 hr1)
    · simp only [hg, Set.indicator_of_notMem hn]
      exact summable_zero
```
targets/erdos-257/nodes/spec-137537c8/Proof.lean, lines 65–74 at fe2c9c743e97 ↗
1. hrow_summable.s1 case
  Leaves Summable fun (j : ℕ) => g (n, j), with hn : n ∈ B.
  Uses library Set.indicator_of_mem, summable_nat_add_iff, summable_geometric_of_lt_one.
  Lean, lines 68–72
  · have hn0 : 0 < n := hn.2 simp only [hg, Set.indicator_of_mem hn] have hr0 : (0 : ℝ) ≤ (1 / 2 : ℝ) ^ n := by positivity have hr1 : (1 / 2 : ℝ) ^ n < 1 := pow_lt_one₀ (by norm_num) (by norm_num) hn0.ne' exact (summable_nat_add_iff 1).mpr (summable_geometric_of_lt_one hr0 hr1)
  targets/erdos-257/nodes/spec-137537c8/Proof.lean, lines 68–72 at fe2c9c743e97 ↗
  hrow_summable.s1.hn0 have (0 : ℕ) < n
  Leaves Summable fun (j : ℕ) => g (n, j), with hn0 : (0 : ℕ) < n.
  Lean, line 68
  · have hn0 : 0 < n := hn.2
  targets/erdos-257/nodes/spec-137537c8/Proof.lean, line 68 at fe2c9c743e97 ↗
  hrow_summable.s1.hr0 have (0 : ℝ) ≤ (1 / 2 : ℝ) ^ n routine: positivity
  Leaves Summable fun (j : ℕ) => ((1 / 2 : ℝ) ^ n) ^ (j + (1 : ℕ)), with hr0 : (0 : ℝ) ≤ (1 / 2 : ℝ) ^ n.
  Lean, line 70
  have hr0 : (0 : ℝ) ≤ (1 / 2 : ℝ) ^ n := by positivity
  targets/erdos-257/nodes/spec-137537c8/Proof.lean, line 70 at fe2c9c743e97 ↗
  hrow_summable.s1.hr1 have (1 / 2 : ℝ) ^ n < (1 : ℝ)
  Leaves Summable fun (j : ℕ) => ((1 / 2 : ℝ) ^ n) ^ (j + (1 : ℕ)), with hr1 : (1 / 2 : ℝ) ^ n < (1 : ℝ).
  Uses library pow_lt_one₀.
  Lean, line 71
  have hr1 : (1 / 2 : ℝ) ^ n < 1 := pow_lt_one₀ (by norm_num) (by norm_num) hn0.ne'
  targets/erdos-257/nodes/spec-137537c8/Proof.lean, line 71 at fe2c9c743e97 ↗
2. hrow_summable.s2 case
  Leaves Summable fun (j : ℕ) => g (n, j), with hn : n ∉ B.
  Uses library Set.indicator_of_notMem, summable_zero.
  Lean, lines 73–74
  · simp only [hg, Set.indicator_of_notMem hn] exact summable_zero
  targets/erdos-257/nodes/spec-137537c8/Proof.lean, lines 73–74 at fe2c9c743e97 ↗
he_summable have Summable e
Leaves ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) = ∑' (m : ℕ), (↑{a : ℕ | a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m}.ncard : ℝ) / (2 : ℝ) ^ m, with he_summable : Summable e.
Uses library Summable.
Lean, line 75
```
  have he_summable : Summable e := lam_summable
```
targets/erdos-257/nodes/spec-137537c8/Proof.lean, line 75 at fe2c9c743e97 ↗
hg_summable have Summable g
Leaves ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) = ∑' (m : ℕ), (↑{a : ℕ | a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m}.ncard : ℝ) / (2 : ℝ) ^ m, with hg_summable : Summable g.
Uses library Summable, summable_prod_of_nonneg, And.intro.
Lean, lines 76–80
```
  have hg_summable : Summable g := by
    rw [summable_prod_of_nonneg hg_nonneg]
    refine ⟨hrow_summable, ?_⟩
    simp_rw [hrow]
    exact he_summable.indicator B
```
targets/erdos-257/nodes/spec-137537c8/Proof.lean, lines 76–80 at fe2c9c743e97 ↗
hL have ∑' (n : (↑A : Type)), e (↑n : ℕ) = ∑' (n : ℕ), B.indicator e n
Leaves ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) = ∑' (m : ℕ), (↑{a : ℕ | a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m}.ncard : ℝ) / (2 : ℝ) ^ m, with hL : ∑' (n : (↑A : Type)), e (↑n : ℕ) = ∑' (n : ℕ), B.indicator e n.
Uses library tsum_subtype, tsum_congr.
Lean, lines 82–94
```
  have hL : ∑' n : A, e n = ∑' n : ℕ, B.indicator e n := by
    rw [tsum_subtype A e]
    apply tsum_congr
    intro n
    by_cases hn : n ∈ A
    · by_cases hn0 : n = 0
      · subst hn0
        rw [Set.indicator_of_notMem h0B, Set.indicator_of_mem hn]
        simp [he]
      · have hnB : n ∈ B := ⟨hn, Nat.pos_of_ne_zero hn0⟩
        rw [Set.indicator_of_mem hn, Set.indicator_of_mem hnB]
    · have hnB : n ∉ B := fun h => hn h.1
      rw [Set.indicator_of_notMem hn, Set.indicator_of_notMem hnB]
```
targets/erdos-257/nodes/spec-137537c8/Proof.lean, lines 82–94 at fe2c9c743e97 ↗
1. hL.s1 case
  Leaves A.indicator e n = B.indicator e n, with hn : n ∈ A.
  Lean, lines 87–92
  · by_cases hn0 : n = 0 · subst hn0 rw [Set.indicator_of_notMem h0B, Set.indicator_of_mem hn] simp [he] · have hnB : n ∈ B := ⟨hn, Nat.pos_of_ne_zero hn0⟩ rw [Set.indicator_of_mem hn, Set.indicator_of_mem hnB]
  targets/erdos-257/nodes/spec-137537c8/Proof.lean, lines 87–92 at fe2c9c743e97 ↗
  hL.s1.s1 case
  Leaves A.indicator e n = B.indicator e n, with hn0 : n = (0 : ℕ).
  Uses library Set.indicator_of_notMem, Set.indicator_of_mem.
  Lean, lines 88–90
  · subst hn0 rw [Set.indicator_of_notMem h0B, Set.indicator_of_mem hn] simp [he]
  targets/erdos-257/nodes/spec-137537c8/Proof.lean, lines 88–90 at fe2c9c743e97 ↗
  hL.s1.s2 case
  Leaves A.indicator e n = B.indicator e n, with hn0 : ¬n = (0 : ℕ).
  Uses library Set.indicator_of_mem.
  Lean, lines 91–92
  · have hnB : n ∈ B := ⟨hn, Nat.pos_of_ne_zero hn0⟩ rw [Set.indicator_of_mem hn, Set.indicator_of_mem hnB]
  targets/erdos-257/nodes/spec-137537c8/Proof.lean, lines 91–92 at fe2c9c743e97 ↗
  hL.s1.s2.hnB have n ∈ B
  Leaves A.indicator e n = B.indicator e n, with hnB : n ∈ B.
  Uses library And.intro, Nat.pos_of_ne_zero.
  Lean, line 91
  · have hnB : n ∈ B := ⟨hn, Nat.pos_of_ne_zero hn0⟩
  targets/erdos-257/nodes/spec-137537c8/Proof.lean, line 91 at fe2c9c743e97 ↗
2. hL.s2 case
  Leaves A.indicator e n = B.indicator e n, with hn : n ∉ A.
  Uses library Set.indicator_of_notMem.
  Lean, lines 93–94
  · have hnB : n ∉ B := fun h => hn h.1 rw [Set.indicator_of_notMem hn, Set.indicator_of_notMem hnB]
  targets/erdos-257/nodes/spec-137537c8/Proof.lean, lines 93–94 at fe2c9c743e97 ↗
  hL.s2.hnB have n ∉ B
  Leaves A.indicator e n = B.indicator e n, with hnB : n ∉ B.
  Lean, line 93
  · have hnB : n ∉ B := fun h => hn h.1
  targets/erdos-257/nodes/spec-137537c8/Proof.lean, line 93 at fe2c9c743e97 ↗
hmid have ∑' (n : ℕ), B.indicator e n = ∑' (p : ℕ × ℕ), g p
Leaves ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) = ∑' (m : ℕ), (↑{a : ℕ | a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m}.ncard : ℝ) / (2 : ℝ) ^ m, with hmid : ∑' (n : ℕ), B.indicator e n = ∑' (p : ℕ × ℕ), g p.
Lean, lines 96–98
```
  have hmid : ∑' n : ℕ, B.indicator e n = ∑' p : ℕ × ℕ, g p := by
    rw [hg_summable.tsum_prod]
    simp_rw [hrow]
```
targets/erdos-257/nodes/spec-137537c8/Proof.lean, lines 96–98 at fe2c9c743e97 ↗
hfib have HasSum (fun (m : ℕ) => ∑' (p : (↑(φ ⁻¹' {m}) : Type)), g (↑p : ℕ × ℕ)) (∑' (p : ℕ × ℕ), g p)
Leaves ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) = ∑' (m : ℕ), (↑{a : ℕ | a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m}.ncard : ℝ) / (2 : ℝ) ^ m, with hfib : HasSum (fun (m : ℕ) => ∑' (p : (↑(φ ⁻¹' {m}) : Type)), g (↑p : ℕ × ℕ)) (∑' (p : ℕ × ℕ), g p).
Uses library HasSum.
Lean, lines 101–102
```
  have hfib : HasSum (fun m => ∑' p : (φ ⁻¹' {m}), g p) (∑' p, g p) :=
    hg_summable.hasSum.tsum_fiberwise φ
```
targets/erdos-257/nodes/spec-137537c8/Proof.lean, lines 101–102 at fe2c9c743e97 ↗

hR have

∑' (p : ℕ × ℕ), g p = ∑' (m : ℕ), (↑{a : ℕ | a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m}.ncard : ℝ) / (2 : ℝ) ^ m

Leaves ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) = ∑' (m : ℕ), (↑{a : ℕ | a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m}.ncard : ℝ) / (2 : ℝ) ^ m, with hR : ∑' (p : ℕ × ℕ), g p = ∑' (m : ℕ), (↑{a : ℕ | a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m}.ncard : ℝ) / (2 : ℝ) ^ m.

Uses library Set.ncard, tsum_congr, Nat.eq_zero_or_pos.

Lean, lines 103–174

  have hR : ∑' p : ℕ × ℕ, g p =
      ∑' m : ℕ, (Set.ncard {a ∈ A | 0 < m ∧ a ∣ m} : ℝ) / 2 ^ m := by
    rw [← hfib.tsum_eq]
    apply tsum_congr
    intro m
    rcases Nat.eq_zero_or_pos m with rfl | hm
    · -- the fibre over 0 is the row n = 0, where the indicator vanishes
      have h1 : ∀ p : (φ ⁻¹' {0}), g p = 0 := by
        rintro ⟨⟨n, j⟩, hp⟩
        have hp' : n * (j + 1) = 0 := by
          simpa [hφ] using hp
        have hn : n = 0 := (mul_eq_zero.mp hp').resolve_right (Nat.succ_ne_zero j)
        simp only [hg]
        rw [hn]
        exact Set.indicator_of_notMem h0B _
      have h2 : {a ∈ A | 0 < 0 ∧ a ∣ 0} = ∅ := by
        ext a
        simp
      rw [tsum_congr h1, tsum_zero, h2, Set.ncard_empty]
      simp
    · -- the fibre over m ≥ 1 is finite: one point per divisor of m
      set T : Finset (ℕ × ℕ) := (Nat.divisors m).image (fun d => (d, m / d - 1)) with hT
      have hsupp : ∀ p ∉ T, (φ ⁻¹' {m}).indicator g p = 0 := by
        rintro ⟨n, j⟩ hp
        by_contra hne
        apply hp
        have hmem : (n, j) ∈ φ ⁻¹' {m} := by
          by_contra h
          exact hne (Set.indicator_of_notMem h _)
        have hφm : n * (j + 1) = m := by simpa [hφ] using hmem
        rw [Set.indicator_of_mem hmem] at hne
        have hnB : n ∈ B := by
          by_contra h
          exact hne (by simp only [hg]; exact Set.indicator_of_notMem h _)
        have hn0 : 0 < n := hnB.2
        have hdiv : n ∣ m := ⟨j + 1, hφm.symm⟩
        have hj : m / n - 1 = j := by
          rw [← hφm, Nat.mul_div_cancel_left (j + 1) hn0]
          simp
        rw [hT, Finset.mem_image]
        exact ⟨n, Nat.mem_divisors.mpr ⟨hdiv, hm.ne'⟩, by rw [hj]⟩
      have hinj : Set.InjOn (fun d : ℕ => (d, m / d - 1)) ↑(Nat.divisors m) :=
        fun a _ b _ h => (Prod.mk.inj h).1
      have hS : {a ∈ A | 0 < m ∧ a ∣ m} = ↑((Nat.divisors m).filter (fun a => a ∈ A)) := by
        ext a
        simp only [Set.mem_ofPred_eq, Finset.coe_filter, Nat.mem_divisors]
        constructor
        · rintro ⟨ha, _, hd⟩
          exact ⟨⟨hd, hm.ne'⟩, ha⟩
        · rintro ⟨⟨hd, _⟩, ha⟩
          exact ⟨ha, hm, hd⟩
      rw [tsum_subtype (φ ⁻¹' {m}) g, tsum_eq_sum hsupp, hT, Finset.sum_image hinj]
      have hterm : ∀ d ∈ Nat.divisors m,
          (φ ⁻¹' {m}).indicator g (d, m / d - 1) = if d ∈ A then (1 / 2 : ℝ) ^ m else 0 := by
        intro d hd
        have hd' := Nat.mem_divisors.mp hd
        have hd0 : 0 < d := Nat.pos_of_mem_divisors hd
        have hq : 1 ≤ m / d := Nat.div_pos (Nat.le_of_dvd hm hd'.1) hd0
        have hφd : (d, m / d - 1) ∈ φ ⁻¹' {m} := by
          show d * (m / d - 1 + 1) = m
          rw [Nat.sub_add_cancel hq, Nat.mul_div_cancel' hd'.1]
        rw [Set.indicator_of_mem hφd]
        simp only [hg]
        by_cases hdA : d ∈ A
        · have hdB : d ∈ B := ⟨hdA, hd0⟩
          rw [Set.indicator_of_mem hdB, if_pos hdA, ← pow_mul, Nat.sub_add_cancel hq,
            Nat.mul_div_cancel' hd'.1]
        · have hdB : d ∉ B := fun h => hdA h.1
          rw [Set.indicator_of_notMem hdB, if_neg hdA]
      rw [Finset.sum_congr rfl hterm, ← Finset.sum_filter, Finset.sum_const, nsmul_eq_mul,
        hS, Set.ncard_coe_finset, one_div_pow]
      ring

targets/erdos-257/nodes/spec-137537c8/Proof.lean, lines 103–174 at fe2c9c743e97 ↗

hR.s1 case
Leaves ∑' (p : (↑(φ ⁻¹' {(0 : ℕ)}) : Type)), g (↑p : ℕ × ℕ) = (↑{a : ℕ | a ∈ A ∧ (0 : ℕ) < (0 : ℕ) ∧ a ∣ (0 : ℕ)}.ncard : ℝ) / (2 : ℝ) ^ (0 : ℕ).
Uses library tsum_congr, tsum_zero, Set.ncard_empty.
Lean, lines 109–122
```
    · -- the fibre over 0 is the row n = 0, where the indicator vanishes
      have h1 : ∀ p : (φ ⁻¹' {0}), g p = 0 := by
        rintro ⟨⟨n, j⟩, hp⟩
        have hp' : n * (j + 1) = 0 := by
          simpa [hφ] using hp
        have hn : n = 0 := (mul_eq_zero.mp hp').resolve_right (Nat.succ_ne_zero j)
        simp only [hg]
        rw [hn]
        exact Set.indicator_of_notMem h0B _
      have h2 : {a ∈ A | 0 < 0 ∧ a ∣ 0} = ∅ := by
        ext a
        simp
      rw [tsum_congr h1, tsum_zero, h2, Set.ncard_empty]
      simp
```
targets/erdos-257/nodes/spec-137537c8/Proof.lean, lines 109–122 at fe2c9c743e97 ↗
1. hR.s1.h1 have ∀ (p : (↑(φ ⁻¹' {(0 : ℕ)}) : Type)), g (↑p : ℕ × ℕ) = (0 : ℝ)
  Leaves ∑' (p : (↑(φ ⁻¹' {(0 : ℕ)}) : Type)), g (↑p : ℕ × ℕ) = (↑{a : ℕ | a ∈ A ∧ (0 : ℕ) < (0 : ℕ) ∧ a ∣ (0 : ℕ)}.ncard : ℝ) / (2 : ℝ) ^ (0 : ℕ), with h1 : ∀ (p : (↑(φ ⁻¹' {(0 : ℕ)}) : Type)), g (↑p : ℕ × ℕ) = (0 : ℝ).
  Uses library Set.indicator_of_notMem.
  Lean, lines 110–117
  have h1 : ∀ p : (φ ⁻¹' {0}), g p = 0 := by rintro ⟨⟨n, j⟩, hp⟩ have hp' : n * (j + 1) = 0 := by simpa [hφ] using hp have hn : n = 0 := (mul_eq_zero.mp hp').resolve_right (Nat.succ_ne_zero j) simp only [hg] rw [hn] exact Set.indicator_of_notMem h0B _
  targets/erdos-257/nodes/spec-137537c8/Proof.lean, lines 110–117 at fe2c9c743e97 ↗
  hR.s1.h1.hp' have printed form did not read back: shown as its Lean lines only
  have hp' : n * (j + 1) = 0 := by simpa [hφ] using hp
  targets/erdos-257/nodes/spec-137537c8/Proof.lean, lines 112–113 at fe2c9c743e97 ↗
  hR.s1.h1.hn have printed form did not read back: shown as its Lean lines only
  have hn : n = 0 := (mul_eq_zero.mp hp').resolve_right (Nat.succ_ne_zero j)
  targets/erdos-257/nodes/spec-137537c8/Proof.lean, line 114 at fe2c9c743e97 ↗
2. hR.s1.h2 have {a : ℕ | a ∈ A ∧ (0 : ℕ) < (0 : ℕ) ∧ a ∣ (0 : ℕ)} = ∅
  Leaves ∑' (p : (↑(φ ⁻¹' {(0 : ℕ)}) : Type)), g (↑p : ℕ × ℕ) = (↑{a : ℕ | a ∈ A ∧ (0 : ℕ) < (0 : ℕ) ∧ a ∣ (0 : ℕ)}.ncard : ℝ) / (2 : ℝ) ^ (0 : ℕ), with h2 : {a : ℕ | a ∈ A ∧ (0 : ℕ) < (0 : ℕ) ∧ a ∣ (0 : ℕ)} = ∅.
  Lean, lines 118–120
  have h2 : {a ∈ A | 0 < 0 ∧ a ∣ 0} = ∅ := by ext a simp
  targets/erdos-257/nodes/spec-137537c8/Proof.lean, lines 118–120 at fe2c9c743e97 ↗
hR.s2 case
Leaves ∑' (p : (↑(φ ⁻¹' {m}) : Type)), g (↑p : ℕ × ℕ) = (↑{a : ℕ | a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m}.ncard : ℝ) / (2 : ℝ) ^ m, with hm : m > (0 : ℕ).
Uses library Finset, Nat.divisors, tsum_subtype, tsum_eq_sum, Finset.sum_image, Finset.sum_congr, rfl, Finset.sum_filter, Finset.sum_const, nsmul_eq_mul, Set.ncard_coe_finset, one_div_pow.
Lean, lines 123–174
```
    · -- the fibre over m ≥ 1 is finite: one point per divisor of m
      set T : Finset (ℕ × ℕ) := (Nat.divisors m).image (fun d => (d, m / d - 1)) with hT
      have hsupp : ∀ p ∉ T, (φ ⁻¹' {m}).indicator g p = 0 := by
        rintro ⟨n, j⟩ hp
        by_contra hne
        apply hp
        have hmem : (n, j) ∈ φ ⁻¹' {m} := by
          by_contra h
          exact hne (Set.indicator_of_notMem h _)
        have hφm : n * (j + 1) = m := by simpa [hφ] using hmem
        rw [Set.indicator_of_mem hmem] at hne
        have hnB : n ∈ B := by
          by_contra h
          exact hne (by simp only [hg]; exact Set.indicator_of_notMem h _)
        have hn0 : 0 < n := hnB.2
        have hdiv : n ∣ m := ⟨j + 1, hφm.symm⟩
        have hj : m / n - 1 = j := by
          rw [← hφm, Nat.mul_div_cancel_left (j + 1) hn0]
          simp
        rw [hT, Finset.mem_image]
        exact ⟨n, Nat.mem_divisors.mpr ⟨hdiv, hm.ne'⟩, by rw [hj]⟩
      have hinj : Set.InjOn (fun d : ℕ => (d, m / d - 1)) ↑(Nat.divisors m) :=
        fun a _ b _ h => (Prod.mk.inj h).1
      have hS : {a ∈ A | 0 < m ∧ a ∣ m} = ↑((Nat.divisors m).filter (fun a => a ∈ A)) := by
        ext a
        simp only [Set.mem_ofPred_eq, Finset.coe_filter, Nat.mem_divisors]
        constructor
        · rintro ⟨ha, _, hd⟩
          exact ⟨⟨hd, hm.ne'⟩, ha⟩
        · rintro ⟨⟨hd, _⟩, ha⟩
          exact ⟨ha, hm, hd⟩
      rw [tsum_subtype (φ ⁻¹' {m}) g, tsum_eq_sum hsupp, hT, Finset.sum_image hinj]
      have hterm : ∀ d ∈ Nat.divisors m,
          (φ ⁻¹' {m}).indicator g (d, m / d - 1) = if d ∈ A then (1 / 2 : ℝ) ^ m else 0 := by
        intro d hd
        have hd' := Nat.mem_divisors.mp hd
        have hd0 : 0 < d := Nat.pos_of_mem_divisors hd
        have hq : 1 ≤ m / d := Nat.div_pos (Nat.le_of_dvd hm hd'.1) hd0
        have hφd : (d, m / d - 1) ∈ φ ⁻¹' {m} := by
          show d * (m / d - 1 + 1) = m
          rw [Nat.sub_add_cancel hq, Nat.mul_div_cancel' hd'.1]
        rw [Set.indicator_of_mem hφd]
        simp only [hg]
        by_cases hdA : d ∈ A
        · have hdB : d ∈ B := ⟨hdA, hd0⟩
          rw [Set.indicator_of_mem hdB, if_pos hdA, ← pow_mul, Nat.sub_add_cancel hq,
            Nat.mul_div_cancel' hd'.1]
        · have hdB : d ∉ B := fun h => hdA h.1
          rw [Set.indicator_of_notMem hdB, if_neg hdA]
      rw [Finset.sum_congr rfl hterm, ← Finset.sum_filter, Finset.sum_const, nsmul_eq_mul,
        hS, Set.ncard_coe_finset, one_div_pow]
      ring
```
targets/erdos-257/nodes/spec-137537c8/Proof.lean, lines 123–174 at fe2c9c743e97 ↗
1. hR.s2.hsupp have ∀ p ∉ T, (φ ⁻¹' {m}).indicator g p = (0 : ℝ)
  Leaves ∑' (p : (↑(φ ⁻¹' {m}) : Type)), g (↑p : ℕ × ℕ) = (↑{a : ℕ | a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m}.ncard : ℝ) / (2 : ℝ) ^ m, with hsupp : ∀ p ∉ T, (φ ⁻¹' {m}).indicator g p = (0 : ℝ).
  Uses library Set.indicator_of_mem, Finset.mem_image, Exists.intro, Nat.mem_divisors, And.intro.
  Lean, lines 125–143
  have hsupp : ∀ p ∉ T, (φ ⁻¹' {m}).indicator g p = 0 := by rintro ⟨n, j⟩ hp by_contra hne apply hp have hmem : (n, j) ∈ φ ⁻¹' {m} := by by_contra h exact hne (Set.indicator_of_notMem h _) have hφm : n * (j + 1) = m := by simpa [hφ] using hmem rw [Set.indicator_of_mem hmem] at hne have hnB : n ∈ B := by by_contra h exact hne (by simp only [hg]; exact Set.indicator_of_notMem h _) have hn0 : 0 < n := hnB.2 have hdiv : n ∣ m := ⟨j + 1, hφm.symm⟩ have hj : m / n - 1 = j := by rw [← hφm, Nat.mul_div_cancel_left (j + 1) hn0] simp rw [hT, Finset.mem_image] exact ⟨n, Nat.mem_divisors.mpr ⟨hdiv, hm.ne'⟩, by rw [hj]⟩
  targets/erdos-257/nodes/spec-137537c8/Proof.lean, lines 125–143 at fe2c9c743e97 ↗
  hR.s2.hsupp.hmem have (n, j) ∈ φ ⁻¹' {m}
  Leaves (n, j) ∈ T, with hmem : (n, j) ∈ φ ⁻¹' {m}.
  Uses library Set.indicator_of_notMem.
  Lean, lines 129–131
  have hmem : (n, j) ∈ φ ⁻¹' {m} := by by_contra h exact hne (Set.indicator_of_notMem h _)
  targets/erdos-257/nodes/spec-137537c8/Proof.lean, lines 129–131 at fe2c9c743e97 ↗
  hR.s2.hsupp.h_x3c6m (hφm) have n * (j + (1 : ℕ)) = m
  Leaves (n, j) ∈ T, with hφm : n * (j + (1 : ℕ)) = m.
  Lean, line 132
  have hφm : n * (j + 1) = m := by simpa [hφ] using hmem
  targets/erdos-257/nodes/spec-137537c8/Proof.lean, line 132 at fe2c9c743e97 ↗
  hR.s2.hsupp.hnB have n ∈ B
  Leaves (n, j) ∈ T, with hnB : n ∈ B.
  Uses library Set.indicator_of_notMem.
  Lean, lines 134–136
  have hnB : n ∈ B := by by_contra h exact hne (by simp only [hg]; exact Set.indicator_of_notMem h _)
  targets/erdos-257/nodes/spec-137537c8/Proof.lean, lines 134–136 at fe2c9c743e97 ↗
  hR.s2.hsupp.hn0 have (0 : ℕ) < n
  Leaves (n, j) ∈ T, with hn0 : (0 : ℕ) < n.
  Lean, line 137
  have hn0 : 0 < n := hnB.2
  targets/erdos-257/nodes/spec-137537c8/Proof.lean, line 137 at fe2c9c743e97 ↗
  hR.s2.hsupp.hdiv have n ∣ m
  Leaves (n, j) ∈ T, with hdiv : n ∣ m.
  Uses library Exists.intro.
  Lean, line 138
  have hdiv : n ∣ m := ⟨j + 1, hφm.symm⟩
  targets/erdos-257/nodes/spec-137537c8/Proof.lean, line 138 at fe2c9c743e97 ↗
  hR.s2.hsupp.hj have m / n - (1 : ℕ) = j
  Leaves (n, j) ∈ T, with hj : m / n - (1 : ℕ) = j.
  Uses library Nat.mul_div_cancel_left.
  Lean, lines 139–141
  have hj : m / n - 1 = j := by rw [← hφm, Nat.mul_div_cancel_left (j + 1) hn0] simp
  targets/erdos-257/nodes/spec-137537c8/Proof.lean, lines 139–141 at fe2c9c743e97 ↗
2. hR.s2.hinj have Set.InjOn (fun (d : ℕ) => (d, m / d - (1 : ℕ))) (↑m.divisors : Set ℕ)
  Leaves ∑' (p : (↑(φ ⁻¹' {m}) : Type)), g (↑p : ℕ × ℕ) = (↑{a : ℕ | a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m}.ncard : ℝ) / (2 : ℝ) ^ m, with hinj : Set.InjOn (fun (d : ℕ) => (d, m / d - (1 : ℕ))) (↑m.divisors : Set ℕ).
  Uses library Set.InjOn, Nat.divisors, Prod.mk.inj.
  Lean, lines 144–145
  have hinj : Set.InjOn (fun d : ℕ => (d, m / d - 1)) ↑(Nat.divisors m) := fun a _ b _ h => (Prod.mk.inj h).1
  targets/erdos-257/nodes/spec-137537c8/Proof.lean, lines 144–145 at fe2c9c743e97 ↗
3. hR.s2.hS have {a : ℕ | a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m} = (↑({a ∈ m.divisors | a ∈ A}) : Set ℕ)
  Leaves ∑' (p : (↑(φ ⁻¹' {m}) : Type)), g (↑p : ℕ × ℕ) = (↑{a : ℕ | a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m}.ncard : ℝ) / (2 : ℝ) ^ m, with hS : {a : ℕ | a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m} = (↑({a ∈ m.divisors | a ∈ A}) : Set ℕ).
  Uses library Nat.divisors, Set.mem_ofPred_eq, Finset.coe_filter, Nat.mem_divisors.
  Lean, lines 146–153
  have hS : {a ∈ A | 0 < m ∧ a ∣ m} = ↑((Nat.divisors m).filter (fun a => a ∈ A)) := by ext a simp only [Set.mem_ofPred_eq, Finset.coe_filter, Nat.mem_divisors] constructor · rintro ⟨ha, _, hd⟩ exact ⟨⟨hd, hm.ne'⟩, ha⟩ · rintro ⟨⟨hd, _⟩, ha⟩ exact ⟨ha, hm, hd⟩
  targets/erdos-257/nodes/spec-137537c8/Proof.lean, lines 146–153 at fe2c9c743e97 ↗
  hR.s2.hS.s1 case
  Leaves a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m → (a ∣ m ∧ m ≠ (0 : ℕ)) ∧ a ∈ A.
  Uses library And.intro.
  Lean, lines 150–151
  · rintro ⟨ha, _, hd⟩ exact ⟨⟨hd, hm.ne'⟩, ha⟩
  targets/erdos-257/nodes/spec-137537c8/Proof.lean, lines 150–151 at fe2c9c743e97 ↗
  hR.s2.hS.s2 case
  Leaves (a ∣ m ∧ m ≠ (0 : ℕ)) ∧ a ∈ A → a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m.
  Uses library And.intro.
  Lean, lines 152–153
  · rintro ⟨⟨hd, _⟩, ha⟩ exact ⟨ha, hm, hd⟩
  targets/erdos-257/nodes/spec-137537c8/Proof.lean, lines 152–153 at fe2c9c743e97 ↗
4. hR.s2.hterm have ∀ d ∈ m.divisors, (φ ⁻¹' {m}).indicator g (d, m / d - (1 : ℕ)) = if d ∈ A then (1 / 2 : ℝ) ^ m else (0 : ℝ)
  Leaves ∑ x ∈ m.divisors, (φ ⁻¹' {m}).indicator g (x, m / x - (1 : ℕ)) = (↑{a : ℕ | a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m}.ncard : ℝ) / (2 : ℝ) ^ m, with hterm : ∀ d ∈ m.divisors, (φ ⁻¹' {m}).indicator g (d, m / d - (1 : ℕ)) = if d ∈ A then (1 / 2 : ℝ) ^ m else (0 : ℝ).
  Uses library Nat.divisors, Set.indicator_of_mem.
  Lean, lines 155–171
  have hterm : ∀ d ∈ Nat.divisors m, (φ ⁻¹' {m}).indicator g (d, m / d - 1) = if d ∈ A then (1 / 2 : ℝ) ^ m else 0 := by intro d hd have hd' := Nat.mem_divisors.mp hd have hd0 : 0 < d := Nat.pos_of_mem_divisors hd have hq : 1 ≤ m / d := Nat.div_pos (Nat.le_of_dvd hm hd'.1) hd0 have hφd : (d, m / d - 1) ∈ φ ⁻¹' {m} := by show d * (m / d - 1 + 1) = m rw [Nat.sub_add_cancel hq, Nat.mul_div_cancel' hd'.1] rw [Set.indicator_of_mem hφd] simp only [hg] by_cases hdA : d ∈ A · have hdB : d ∈ B := ⟨hdA, hd0⟩ rw [Set.indicator_of_mem hdB, if_pos hdA, ← pow_mul, Nat.sub_add_cancel hq, Nat.mul_div_cancel' hd'.1] · have hdB : d ∉ B := fun h => hdA h.1 rw [Set.indicator_of_notMem hdB, if_neg hdA]
  targets/erdos-257/nodes/spec-137537c8/Proof.lean, lines 155–171 at fe2c9c743e97 ↗
  hR.s2.hterm.hd' have d ∣ m ∧ m ≠ (0 : ℕ)
  Leaves (φ ⁻¹' {m}).indicator g (d, m / d - (1 : ℕ)) = if d ∈ A then (1 / 2 : ℝ) ^ m else (0 : ℝ), with hd' : d ∣ m ∧ m ≠ (0 : ℕ).
  Uses library Nat.mem_divisors.
  Lean, line 158
  have hd' := Nat.mem_divisors.mp hd
  targets/erdos-257/nodes/spec-137537c8/Proof.lean, line 158 at fe2c9c743e97 ↗
  hR.s2.hterm.hd0 have (0 : ℕ) < d
  Leaves (φ ⁻¹' {m}).indicator g (d, m / d - (1 : ℕ)) = if d ∈ A then (1 / 2 : ℝ) ^ m else (0 : ℝ), with hd0 : (0 : ℕ) < d.
  Uses library Nat.pos_of_mem_divisors.
  Lean, line 159
  have hd0 : 0 < d := Nat.pos_of_mem_divisors hd
  targets/erdos-257/nodes/spec-137537c8/Proof.lean, line 159 at fe2c9c743e97 ↗
  hR.s2.hterm.hq have (1 : ℕ) ≤ m / d
  Leaves (φ ⁻¹' {m}).indicator g (d, m / d - (1 : ℕ)) = if d ∈ A then (1 / 2 : ℝ) ^ m else (0 : ℝ), with hq : (1 : ℕ) ≤ m / d.
  Uses library Nat.div_pos, Nat.le_of_dvd.
  Lean, line 160
  have hq : 1 ≤ m / d := Nat.div_pos (Nat.le_of_dvd hm hd'.1) hd0
  targets/erdos-257/nodes/spec-137537c8/Proof.lean, line 160 at fe2c9c743e97 ↗
  hR.s2.hterm.h_x3c6d (hφd) have (d, m / d - (1 : ℕ)) ∈ φ ⁻¹' {m}
  Leaves (φ ⁻¹' {m}).indicator g (d, m / d - (1 : ℕ)) = if d ∈ A then (1 / 2 : ℝ) ^ m else (0 : ℝ), with hφd : (d, m / d - (1 : ℕ)) ∈ φ ⁻¹' {m}.
  Uses library Nat.sub_add_cancel, Nat.mul_div_cancel'.
  Lean, lines 161–163
  have hφd : (d, m / d - 1) ∈ φ ⁻¹' {m} := by show d * (m / d - 1 + 1) = m rw [Nat.sub_add_cancel hq, Nat.mul_div_cancel' hd'.1]
  targets/erdos-257/nodes/spec-137537c8/Proof.lean, lines 161–163 at fe2c9c743e97 ↗
  hR.s2.hterm.s5 case
  Leaves B.indicator (fun (n : ℕ) => ((1 / 2 : ℝ) ^ n) ^ (m / d - (1 : ℕ) + (1 : ℕ))) d = if d ∈ A then (1 / 2 : ℝ) ^ m else (0 : ℝ), with hdA : d ∈ A.
  Uses library Set.indicator_of_mem, if_pos, pow_mul, Nat.sub_add_cancel, Nat.mul_div_cancel'.
  Lean, lines 167–169
  · have hdB : d ∈ B := ⟨hdA, hd0⟩ rw [Set.indicator_of_mem hdB, if_pos hdA, ← pow_mul, Nat.sub_add_cancel hq, Nat.mul_div_cancel' hd'.1]
  targets/erdos-257/nodes/spec-137537c8/Proof.lean, lines 167–169 at fe2c9c743e97 ↗
  hR.s2.hterm.s5.hdB have d ∈ B
  Leaves B.indicator (fun (n : ℕ) => ((1 / 2 : ℝ) ^ n) ^ (m / d - (1 : ℕ) + (1 : ℕ))) d = if d ∈ A then (1 / 2 : ℝ) ^ m else (0 : ℝ), with hdB : d ∈ B.
  Uses library And.intro.
  Lean, line 167
  · have hdB : d ∈ B := ⟨hdA, hd0⟩
  targets/erdos-257/nodes/spec-137537c8/Proof.lean, line 167 at fe2c9c743e97 ↗
  hR.s2.hterm.s6 case
  Leaves B.indicator (fun (n : ℕ) => ((1 / 2 : ℝ) ^ n) ^ (m / d - (1 : ℕ) + (1 : ℕ))) d = if d ∈ A then (1 / 2 : ℝ) ^ m else (0 : ℝ), with hdA : d ∉ A.
  Uses library Set.indicator_of_notMem, if_neg.
  Lean, lines 170–171
  · have hdB : d ∉ B := fun h => hdA h.1 rw [Set.indicator_of_notMem hdB, if_neg hdA]
  targets/erdos-257/nodes/spec-137537c8/Proof.lean, lines 170–171 at fe2c9c743e97 ↗
  hR.s2.hterm.s6.hdB have d ∉ B
  Leaves B.indicator (fun (n : ℕ) => ((1 / 2 : ℝ) ^ n) ^ (m / d - (1 : ℕ) + (1 : ℕ))) d = if d ∈ A then (1 / 2 : ℝ) ^ m else (0 : ℝ), with hdB : d ∉ B.
  Lean, line 170
  · have hdB : d ∉ B := fun h => hdA h.1
  targets/erdos-257/nodes/spec-137537c8/Proof.lean, line 170 at fe2c9c743e97 ↗

The proof in Lean (Proof.lean)

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

Proof.lean — its sha256 is the artifact_hash of the attestation below, so these are the bytes the gate checked. Rendered from targets/erdos-257/nodes/spec-137537c8/Proof.lean, sha256 4dc304abe5ef.

import Mathlib
import Nodes.«spec-137537c8».Context

private lemma lam_term_le (n : ℕ) : (1 : ℝ) / (2 ^ n - 1) ≤ 2 * (1 / 2 : ℝ) ^ n := by
  rcases Nat.eq_zero_or_pos n with rfl | hn
  · norm_num
  · have h1 : (2 : ℝ) ≤ 2 ^ n := by
      calc (2 : ℝ) = 2 ^ 1 := by norm_num
        _ ≤ 2 ^ n := pow_le_pow_right₀ (by norm_num) hn
    have hpos : (0 : ℝ) < 2 ^ n - 1 := by linarith
    rw [div_le_iff₀ hpos, one_div_pow, mul_comm]
    have h2 : (2 : ℝ) ^ n * (1 / 2 ^ n) = 1 := by field_simp
    have h3 : 0 < (1 : ℝ) / 2 ^ n := by positivity
    nlinarith

private lemma lam_term_nonneg (n : ℕ) : (0 : ℝ) ≤ 1 / (2 ^ n - 1) := by
  rcases Nat.eq_zero_or_pos n with rfl | hn
  · norm_num
  · have h1 : (1 : ℝ) ≤ 2 ^ n := one_le_pow₀ (by norm_num)
    exact div_nonneg zero_le_one (by linarith)

private lemma lam_summable : Summable (fun n : ℕ => (1 : ℝ) / (2 ^ n - 1)) :=
  Summable.of_nonneg_of_le lam_term_nonneg lam_term_le ((summable_geometric_two).mul_left 2)

/- For `n ≥ 1`, `1/(2^n - 1) = ∑_{j ≥ 1} (2^{-n})^j`: the geometric series behind the Lambert identity. -/
private lemma lam_term_eq_tsum {n : ℕ} (hn : 0 < n) :
    (1 : ℝ) / (2 ^ n - 1) = ∑' j : ℕ, ((1 / 2 : ℝ) ^ n) ^ (j + 1) := by
  have hr0 : (0 : ℝ) ≤ (1 / 2 : ℝ) ^ n := by positivity
  have hr1 : (1 / 2 : ℝ) ^ n < 1 := pow_lt_one₀ (by norm_num) (by norm_num) hn.ne'
  have h2 : (1 : ℝ) < 2 ^ n := one_lt_pow₀ (by norm_num) hn.ne'
  have h3 : (2 : ℝ) ^ n - 1 ≠ 0 := ne_of_gt (by linarith)
  have h4 : (1 : ℝ) - (1 / 2 : ℝ) ^ n ≠ 0 := ne_of_gt (by linarith)
  simp_rw [pow_succ]
  rw [tsum_mul_right, tsum_geometric_of_lt_one hr0 hr1]
  rw [one_div_pow] at h4 ⊢
  field_simp

/-- The Lambert identity for Erdős 257: for every `A ⊆ ℕ`, the sum `∑_{a ∈ A} 1/(2^a - 1)` is the
binary series `∑_{m ≥ 1} f_A(m) / 2^m` whose `m`-th coefficient `f_A(m) = #{a ∈ A : a ∣ m}` counts
the divisors of `m` that lie in `A`. It is the first line of every published irrationality
argument for this problem (Erdős 1948 with `f_ℕ = d`, Erdős 1968, Luca–Tachiya 2014,
Duverney–Tachiya 2019, Tao–Teräväinen with `f = ω`) and of the carry bookkeeping of the
greedy walk. The term at `m = 0` is `0` (the set `{a ∈ A | 0 < m ∧ a ∣ m}` is empty there), and
in Lean a `0 ∈ A` contributes `1/0 = 0` on the left and divides no `m ≥ 1` on the right, so no
hypothesis on `A` is needed. -/
theorem Opn.erdos_257_lambert_identity :
    ∀ (A : Set ℕ),
    ∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1) =
      ∑' m : ℕ, (Set.ncard {a ∈ A | 0 < m ∧ a ∣ m} : ℝ) / 2 ^ m := by
  intro A
  classical
  set e : ℕ → ℝ := fun n => (1 : ℝ) / (2 ^ n - 1) with he
  set B : Set ℕ := A ∩ Set.Ioi 0 with hB
  have h0B : (0 : ℕ) ∉ B := fun h => lt_irrefl 0 h.2
  set g : ℕ × ℕ → ℝ := fun p => B.indicator (fun n => ((1 / 2 : ℝ) ^ n) ^ (p.2 + 1)) p.1 with hg
  have hg_nonneg : ∀ p, 0 ≤ g p := fun p => Set.indicator_nonneg (fun n _ => by positivity) _
  -- each row of `g` sums to the term of `e`
  have hrow : ∀ n, ∑' j, g (n, j) = B.indicator e n := by
    intro n
    by_cases hn : n ∈ B
    · have hn0 : 0 < n := hn.2
      simp only [hg, Set.indicator_of_mem hn, he]
      exact (lam_term_eq_tsum hn0).symm
    · simp only [hg, Set.indicator_of_notMem hn, tsum_zero]
  have hrow_summable : ∀ n, Summable (fun j => g (n, j)) := by
    intro n
    by_cases hn : n ∈ B
    · have hn0 : 0 < n := hn.2
      simp only [hg, Set.indicator_of_mem hn]
      have hr0 : (0 : ℝ) ≤ (1 / 2 : ℝ) ^ n := by positivity
      have hr1 : (1 / 2 : ℝ) ^ n < 1 := pow_lt_one₀ (by norm_num) (by norm_num) hn0.ne'
      exact (summable_nat_add_iff 1).mpr (summable_geometric_of_lt_one hr0 hr1)
    · simp only [hg, Set.indicator_of_notMem hn]
      exact summable_zero
  have he_summable : Summable e := lam_summable
  have hg_summable : Summable g := by
    rw [summable_prod_of_nonneg hg_nonneg]
    refine ⟨hrow_summable, ?_⟩
    simp_rw [hrow]
    exact he_summable.indicator B
  -- the left side as a sum over ℕ of the indicator of `B`
  have hL : ∑' n : A, e n = ∑' n : ℕ, B.indicator e n := by
    rw [tsum_subtype A e]
    apply tsum_congr
    intro n
    by_cases hn : n ∈ A
    · by_cases hn0 : n = 0
      · subst hn0
        rw [Set.indicator_of_notMem h0B, Set.indicator_of_mem hn]
        simp [he]
      · have hnB : n ∈ B := ⟨hn, Nat.pos_of_ne_zero hn0⟩
        rw [Set.indicator_of_mem hn, Set.indicator_of_mem hnB]
    · have hnB : n ∉ B := fun h => hn h.1
      rw [Set.indicator_of_notMem hn, Set.indicator_of_notMem hnB]
  -- the double series, summed row by row
  have hmid : ∑' n : ℕ, B.indicator e n = ∑' p : ℕ × ℕ, g p := by
    rw [hg_summable.tsum_prod]
    simp_rw [hrow]
  -- the double series, summed along the fibres of `(n, j) ↦ n * (j + 1)`
  set φ : ℕ × ℕ → ℕ := fun p => p.1 * (p.2 + 1) with hφ
  have hfib : HasSum (fun m => ∑' p : (φ ⁻¹' {m}), g p) (∑' p, g p) :=
    hg_summable.hasSum.tsum_fiberwise φ
  have hR : ∑' p : ℕ × ℕ, g p =
      ∑' m : ℕ, (Set.ncard {a ∈ A | 0 < m ∧ a ∣ m} : ℝ) / 2 ^ m := by
    rw [← hfib.tsum_eq]
    apply tsum_congr
    intro m
    rcases Nat.eq_zero_or_pos m with rfl | hm
    · -- the fibre over 0 is the row n = 0, where the indicator vanishes
      have h1 : ∀ p : (φ ⁻¹' {0}), g p = 0 := by
        rintro ⟨⟨n, j⟩, hp⟩
        have hp' : n * (j + 1) = 0 := by
          simpa [hφ] using hp
        have hn : n = 0 := (mul_eq_zero.mp hp').resolve_right (Nat.succ_ne_zero j)
        simp only [hg]
        rw [hn]
        exact Set.indicator_of_notMem h0B _
      have h2 : {a ∈ A | 0 < 0 ∧ a ∣ 0} = ∅ := by
        ext a
        simp
      rw [tsum_congr h1, tsum_zero, h2, Set.ncard_empty]
      simp
    · -- the fibre over m ≥ 1 is finite: one point per divisor of m
      set T : Finset (ℕ × ℕ) := (Nat.divisors m).image (fun d => (d, m / d - 1)) with hT
      have hsupp : ∀ p ∉ T, (φ ⁻¹' {m}).indicator g p = 0 := by
        rintro ⟨n, j⟩ hp
        by_contra hne
        apply hp
        have hmem : (n, j) ∈ φ ⁻¹' {m} := by
          by_contra h
          exact hne (Set.indicator_of_notMem h _)
        have hφm : n * (j + 1) = m := by simpa [hφ] using hmem
        rw [Set.indicator_of_mem hmem] at hne
        have hnB : n ∈ B := by
          by_contra h
          exact hne (by simp only [hg]; exact Set.indicator_of_notMem h _)
        have hn0 : 0 < n := hnB.2
        have hdiv : n ∣ m := ⟨j + 1, hφm.symm⟩
        have hj : m / n - 1 = j := by
          rw [← hφm, Nat.mul_div_cancel_left (j + 1) hn0]
          simp
        rw [hT, Finset.mem_image]
        exact ⟨n, Nat.mem_divisors.mpr ⟨hdiv, hm.ne'⟩, by rw [hj]⟩
      have hinj : Set.InjOn (fun d : ℕ => (d, m / d - 1)) ↑(Nat.divisors m) :=
        fun a _ b _ h => (Prod.mk.inj h).1
      have hS : {a ∈ A | 0 < m ∧ a ∣ m} = ↑((Nat.divisors m).filter (fun a => a ∈ A)) := by
        ext a
        simp only [Set.mem_ofPred_eq, Finset.coe_filter, Nat.mem_divisors]
        constructor
        · rintro ⟨ha, _, hd⟩
          exact ⟨⟨hd, hm.ne'⟩, ha⟩
        · rintro ⟨⟨hd, _⟩, ha⟩
          exact ⟨ha, hm, hd⟩
      rw [tsum_subtype (φ ⁻¹' {m}) g, tsum_eq_sum hsupp, hT, Finset.sum_image hinj]
      have hterm : ∀ d ∈ Nat.divisors m,
          (φ ⁻¹' {m}).indicator g (d, m / d - 1) = if d ∈ A then (1 / 2 : ℝ) ^ m else 0 := by
        intro d hd
        have hd' := Nat.mem_divisors.mp hd
        have hd0 : 0 < d := Nat.pos_of_mem_divisors hd
        have hq : 1 ≤ m / d := Nat.div_pos (Nat.le_of_dvd hm hd'.1) hd0
        have hφd : (d, m / d - 1) ∈ φ ⁻¹' {m} := by
          show d * (m / d - 1 + 1) = m
          rw [Nat.sub_add_cancel hq, Nat.mul_div_cancel' hd'.1]
        rw [Set.indicator_of_mem hφd]
        simp only [hg]
        by_cases hdA : d ∈ A
        · have hdB : d ∈ B := ⟨hdA, hd0⟩
          rw [Set.indicator_of_mem hdB, if_pos hdA, ← pow_mul, Nat.sub_add_cancel hq,
            Nat.mul_div_cancel' hd'.1]
        · have hdB : d ∉ B := fun h => hdA h.1
          rw [Set.indicator_of_notMem hdB, if_neg hdA]
      rw [Finset.sum_congr rfl hterm, ← Finset.sum_filter, Finset.sum_const, nsmul_eq_mul,
        hS, Set.ncard_coe_finset, one_div_pow]
      ring
  rw [hL, hmid, hR]

What is known

Work on it

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-137537c8».Context

/-- The Lambert identity for Erdős 257: for every `A ⊆ ℕ`, the sum `∑_{a ∈ A} 1/(2^a - 1)` is the
binary series `∑_{m ≥ 1} f_A(m) / 2^m` whose `m`-th coefficient `f_A(m) = #{a ∈ A : a ∣ m}` counts
the divisors of `m` that lie in `A`. It is the first line of every published irrationality
argument for this problem (Erdős 1948 with `f_ℕ = d`, Erdős 1968, Luca–Tachiya 2014,
Duverney–Tachiya 2019, Tao–Teräväinen with `f = ω`) and of the carry bookkeeping of the
greedy walk. The term at `m = 0` is `0` (the set `{a ∈ A | 0 < m ∧ a ∣ m}` is empty there), and
in Lean a `0 ∈ A` contributes `1/0 = 0` on the left and divides no `m ≥ 1` on the right, so no
hypothesis on `A` is needed. -/
theorem Opn.erdos_257_lambert_identity :
    ∀ (A : Set ℕ),
    ∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1) =
      ∑' m : ℕ, (Set.ncard {a ∈ A | 0 < m ∧ a ∣ m} : ℝ) / 2 ^ m := by
  sorry

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

Draft · drafted, by the model named above

$\displaystyle \forall\, A \subseteq \mathbb{N}:\qquad \sum_{a\in A}\frac{1}{2^a-1} \;=\; \sum_{m\ge 1}\frac{f_A(m)}{2^m},\qquad f_A(m) = \#\{a \in A : a \mid m\}.$

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

Rendered from targets/erdos-257/nodes/spec-137537c8/Statement.lean. Origin: authored.

Attestation: pass, 7 of 7 checks

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

Verdict pass, from attestations/000968.json.

Submitter: t1026-c
Toolchain: leanprover/lean4:v4.33.1 (hash f54d0bc916bf76a7fae460ce9d078ccd1f74aeb4fd12c4b6546bca28b6aa1c63)
Mathlib: 0df444a360eaa60ab8c11dca51a86af692955474
Reviewer: none needed (intermediate)

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

Witness

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

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/erdos-257/nodes/spec-137537c8/Witness.lean, sha256 c34bbc1aa8ef.

theorem witness : ∃ (A : Set ℕ), True := ⟨∅, trivial⟩

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

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

Untrusted: acknowledgment of a div-zero finding at 1 / (2 ^ ↑n - 1)

The divisor is zero only at n = 0, where Lean's junk value makes the term 0; the identity holds with that convention, which is why no hypothesis on A is needed.

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

Untrusted: acknowledgment of a div-zero finding at ↑{a | a ∈ A ∧ 0 < m ∧ a ∣ m}.ncard / 2 ^ m

The divisor 2^m is a positive real for every natural m; the guard 0 < m is on the set being counted, not on the divisor.

How to read this page

How to read a statement’s page →

Explainer

Overview

The double series and its summability

The left side as the row-by-row sum

The right side as the sum along the fibres

Overview

The double series and its summability (h0B hg_nonneg hrow hrow_summable he_summable hg_summable)

The left side as the row-by-row sum (hL hmid)

The right side as the sum along the fibres (hfib hR)

How it was proved

What is known

Work on it

Record