FormalConjectures.ErdosProblems.«257»

/-
Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

Erdős Problem 257

Reference: erdosproblems.com/257

namespace Erdos257

Let $A\subseteq\mathbb{N}$ be an infinite set. Is $$ \sum_{n\in A} \frac{1}{2^n - 1} $$ irrational?

@[category research open, AMS 11]
theorem erdos_257 : answer(sorry) ↔ ∀ (A : Set ℕ), A.Infinite →
    Irrational (∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1)) := by⊢ True ↔ ∀ (A : Set ℕ), A.Infinite → Irrational (∑' (n : ↑A), 1 / (2 ^ ↑n - 1))
  sorryAll goals completed! 🐙

Show that $$ \sum_{n} \frac{1}{2^n - 1} = \sum_{n} \frac{d(n)}{2^n}, $$ where $d(n)$ is the number of divisors of $n$.


@[category textbook, AMS 11]
theorem erdos_257.variants.tsum_top_eq :
    ∑' n, 1 / (2 ^ n - 1 : ℝ) = ∑' n, n.divisors.card / (2 ^ n : ℝ) := by⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n
  have hr : ‖(1 / 2 : ℝ)‖ < 1 := by norm_numhr:‖1 / 2‖ < 1⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ nhr:‖1 / 2‖ < 1⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n
  -- The key Lambert-series identity from Mathlib (`k = 0`):
  -- `∑' n:ℕ+, (1/2)^n / (1 - (1/2)^n) = ∑' n:ℕ+, σ 0 n * (1/2)^n`, with summands rewritten.
  have key := tsum_pow_div_one_sub_eq_tsum_sigma (𝕜 := ℝ) hr 0hr:‖1 / 2‖ < 1key:∑' (n : ℕ+), ↑↑n ^ 0 * (1 / 2) ^ ↑n / (1 - (1 / 2) ^ ↑n) =
  ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma 0) ↑n) * (1 / 2) ^ ↑n⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n
  have hpos : ∀ n : ℕ, 0 < n → (2 : ℝ) ≤ 2 ^ n := fun n hn ↦ byhr:‖1 / 2‖ < 1key:∑' (n : ℕ+), ↑↑n ^ 0 * (1 / 2) ^ ↑n / (1 - (1 / 2) ^ ↑n) =
  ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma 0) ↑n) * (1 / 2) ^ ↑nn:ℕhn:0 < n⊢ 2 ≤ 2 ^ nhr:‖1 / 2‖ < 1key:∑' (n : ℕ+), ↑↑n ^ 0 * (1 / 2) ^ ↑n / (1 - (1 / 2) ^ ↑n) =
  ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma 0) ↑n) * (1 / 2) ^ ↑nhpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ n⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n
    simpa using pow_le_pow_right₀ (byhr:‖1 / 2‖ < 1key:∑' (n : ℕ+), ↑↑n ^ 0 * (1 / 2) ^ ↑n / (1 - (1 / 2) ^ ↑n) =
  ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma 0) ↑n) * (1 / 2) ^ ↑nn:ℕhn:0 < n⊢ 1 ≤ 2hr:‖1 / 2‖ < 1key:∑' (n : ℕ+), ↑↑n ^ 0 * (1 / 2) ^ ↑n / (1 - (1 / 2) ^ ↑n) =
  ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma 0) ↑n) * (1 / 2) ^ ↑nhpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ n⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n norm_numAll goals completed! 🐙hr:‖1 / 2‖ < 1key:∑' (n : ℕ+), ↑↑n ^ 0 * (1 / 2) ^ ↑n / (1 - (1 / 2) ^ ↑n) =
  ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma 0) ↑n) * (1 / 2) ^ ↑nhpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ n⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n : (1 : ℝ) ≤ 2) hnhr:‖1 / 2‖ < 1key:∑' (n : ℕ+), ↑↑n ^ 0 * (1 / 2) ^ ↑n / (1 - (1 / 2) ^ ↑n) =
  ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma 0) ↑n) * (1 / 2) ^ ↑nhpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ n⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n
  simp only [pow_zero, one_mul, ArithmeticFunction.sigma_zero_apply,
    show ∀ n : ℕ+, ((1 : ℝ) / 2) ^ (n : ℕ) / (1 - (1 / 2) ^ (n : ℕ))
        = 1 / (2 ^ (n : ℕ) - 1) from fun n ↦ by
      have h := hpos n n.2
      have hp : (0 : ℝ) < 2 ^ (n : ℕ) := by positivity
      have h1 : (1 : ℝ) / 2 ^ (n : ℕ) < 1 := (div_lt_one hp).2 (by linarith)
      rw [div_pow, one_pow, div_eq_div_iff (by linarith) (by linarith)]; field_simp,
    show ∀ n : ℕ+, ((n : ℕ).divisors.card : ℝ) * (1 / 2) ^ (n : ℕ)
        = (n : ℕ).divisors.card / 2 ^ (n : ℕ) from fun n ↦ by
      rw [div_pow, one_pow]; ring] at keyhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑n⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n
  -- Domination by geometric series gives `ℕ`-summability of both sides.
  have hsummL : Summable fun n : ℕ ↦ 1 / (2 ^ n - 1 : ℝ) :=
    .of_nonneg_of_le
      (fun n ↦ byhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nn:ℕ⊢ 0 ≤ 1 / (2 ^ n - 1)hr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n have := one_le_pow₀ (one_le_two (α := ℝ)) (n := n)hr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nn:ℕthis:1 ≤ 2 ^ n⊢ 0 ≤ 1 / (2 ^ n - 1)hr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n; apply div_nonneghahr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nn:ℕthis:1 ≤ 2 ^ n⊢ 0 ≤ 1hbhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nn:ℕthis:1 ≤ 2 ^ n⊢ 0 ≤ 2 ^ n - 1hr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n <;>hahr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nn:ℕthis:1 ≤ 2 ^ n⊢ 0 ≤ 1hbhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nn:ℕthis:1 ≤ 2 ^ n⊢ 0 ≤ 2 ^ n - 1hr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n linarithAll goals completed! 🐙hr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n)
      (fun n ↦ byhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nn:ℕ⊢ 1 / (2 ^ n - 1) ≤ 2 * (1 / 2) ^ nhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n
        rcases Nat.eq_zero_or_pos n with h | hinlhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nn:ℕh:n = 0⊢ 1 / (2 ^ n - 1) ≤ 2 * (1 / 2) ^ ninrhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nn:ℕh:n > 0⊢ 1 / (2 ^ n - 1) ≤ 2 * (1 / 2) ^ nhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n
        ·inlhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nn:ℕh:n = 0⊢ 1 / (2 ^ n - 1) ≤ 2 * (1 / 2) ^ nhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n simp [h]All goals completed! 🐙hr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n
        ·inrhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nn:ℕh:n > 0⊢ 1 / (2 ^ n - 1) ≤ 2 * (1 / 2) ^ nhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n have h2 := hpos n hinrhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nn:ℕh:n > 0h2:2 ≤ 2 ^ n⊢ 1 / (2 ^ n - 1) ≤ 2 * (1 / 2) ^ nhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n
          rw [show (2 : ℝ) * (1 / 2) ^ n = 2 / 2 ^ n byhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nn:ℕ⊢ 1 / (2 ^ n - 1) ≤ 2 * (1 / 2) ^ ninrhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nn:ℕh:n > 0h2:2 ≤ 2 ^ n⊢ 1 * 2 ^ n ≤ 2 * (2 ^ n - 1)hr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n rw [div_pow,hr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nn:ℕh:n > 0h2:2 ≤ 2 ^ n⊢ 2 * (1 ^ n / 2 ^ n) = 2 / 2 ^ nhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nn:ℕh:n > 0h2:2 ≤ 2 ^ n⊢ 2 * (1 / 2 ^ n) = 2 / 2 ^ ninrhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nn:ℕh:n > 0h2:2 ≤ 2 ^ n⊢ 1 * 2 ^ n ≤ 2 * (2 ^ n - 1)hr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n one_powhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nn:ℕh:n > 0h2:2 ≤ 2 ^ n⊢ 2 * (1 / 2 ^ n) = 2 / 2 ^ nhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nn:ℕh:n > 0h2:2 ≤ 2 ^ n⊢ 2 * (1 / 2 ^ n) = 2 / 2 ^ ninrhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nn:ℕh:n > 0h2:2 ≤ 2 ^ n⊢ 1 * 2 ^ n ≤ 2 * (2 ^ n - 1)hr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n]hr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nn:ℕh:n > 0h2:2 ≤ 2 ^ n⊢ 2 * (1 / 2 ^ n) = 2 / 2 ^ ninrhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nn:ℕh:n > 0h2:2 ≤ 2 ^ n⊢ 1 * 2 ^ n ≤ 2 * (2 ^ n - 1)hr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n; ringAll goals completed! 🐙inrhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nn:ℕh:n > 0h2:2 ≤ 2 ^ n⊢ 1 * 2 ^ n ≤ 2 * (2 ^ n - 1)hr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n,
            div_le_div_iff₀ (byhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nn:ℕh:n > 0h2:2 ≤ 2 ^ n⊢ 0 < 2 ^ n - 1inrhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nn:ℕh:n > 0h2:2 ≤ 2 ^ n⊢ 1 * 2 ^ n ≤ 2 * (2 ^ n - 1)hr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n linarithAll goals completed! 🐙inrhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nn:ℕh:n > 0h2:2 ≤ 2 ^ n⊢ 1 * 2 ^ n ≤ 2 * (2 ^ n - 1)hr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n) (byhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nn:ℕh:n > 0h2:2 ≤ 2 ^ n⊢ 0 < 2 ^ ninrhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nn:ℕh:n > 0h2:2 ≤ 2 ^ n⊢ 1 * 2 ^ n ≤ 2 * (2 ^ n - 1)hr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n positivityAll goals completed! 🐙inrhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nn:ℕh:n > 0h2:2 ≤ 2 ^ n⊢ 1 * 2 ^ n ≤ 2 * (2 ^ n - 1)hr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n)]inrhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nn:ℕh:n > 0h2:2 ≤ 2 ^ n⊢ 1 * 2 ^ n ≤ 2 * (2 ^ n - 1)hr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n; nlinarithAll goals completed! 🐙hr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n)
      ((summable_geometric_of_norm_lt_one hr).mul_left 2)hr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n
  have hsummR : Summable fun n : ℕ ↦ (n.divisors.card : ℝ) / (2 ^ n : ℝ) :=
    .of_nonneg_of_le (fun n ↦ byhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)n:ℕ⊢ 0 ≤ ↑n.divisors.card / 2 ^ nhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)hsummR:Summable fun n ↦ ↑n.divisors.card / 2 ^ n⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n positivityAll goals completed! 🐙hr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)hsummR:Summable fun n ↦ ↑n.divisors.card / 2 ^ n⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n)
      (fun n ↦ byhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)n:ℕ⊢ ↑n.divisors.card / 2 ^ n ≤ ↑n ^ 1 * (1 / 2) ^ nhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)hsummR:Summable fun n ↦ ↑n.divisors.card / 2 ^ n⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n
        rw [pow_one,hr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)n:ℕ⊢ ↑n.divisors.card / 2 ^ n ≤ ↑n * (1 / 2) ^ nhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)n:ℕ⊢ ↑n.divisors.card / 2 ^ n ≤ ↑n / 2 ^ nhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)hsummR:Summable fun n ↦ ↑n.divisors.card / 2 ^ n⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n show ((1 : ℝ) / 2) ^ n = 1 / 2 ^ n byhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)n:ℕ⊢ ↑n.divisors.card / 2 ^ n ≤ ↑n ^ 1 * (1 / 2) ^ nhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)n:ℕ⊢ ↑n.divisors.card / 2 ^ n ≤ ↑n / 2 ^ nhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)hsummR:Summable fun n ↦ ↑n.divisors.card / 2 ^ n⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n rw [div_pow,hr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)n:ℕ⊢ 1 ^ n / 2 ^ n = 1 / 2 ^ nAll goals completed! 🐙hr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)n:ℕ⊢ ↑n.divisors.card / 2 ^ n ≤ ↑n / 2 ^ nhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)hsummR:Summable fun n ↦ ↑n.divisors.card / 2 ^ n⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n one_powhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)n:ℕ⊢ 1 / 2 ^ n = 1 / 2 ^ nAll goals completed! 🐙hr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)n:ℕ⊢ ↑n.divisors.card / 2 ^ n ≤ ↑n / 2 ^ nhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)hsummR:Summable fun n ↦ ↑n.divisors.card / 2 ^ n⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n]All goals completed! 🐙hr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)n:ℕ⊢ ↑n.divisors.card / 2 ^ n ≤ ↑n / 2 ^ nhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)hsummR:Summable fun n ↦ ↑n.divisors.card / 2 ^ n⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n, mul_one_divhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)n:ℕ⊢ ↑n.divisors.card / 2 ^ n ≤ ↑n / 2 ^ nhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)n:ℕ⊢ ↑n.divisors.card / 2 ^ n ≤ ↑n / 2 ^ nhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)hsummR:Summable fun n ↦ ↑n.divisors.card / 2 ^ n⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n]hr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)n:ℕ⊢ ↑n.divisors.card / 2 ^ n ≤ ↑n / 2 ^ nhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)hsummR:Summable fun n ↦ ↑n.divisors.card / 2 ^ n⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n
        gcongrahr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)n:ℕ⊢ n.divisors.card ≤ nhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)hsummR:Summable fun n ↦ ↑n.divisors.card / 2 ^ n⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n; exact_mod_cast Nat.card_divisors_le_self nAll goals completed! 🐙hr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)hsummR:Summable fun n ↦ ↑n.divisors.card / 2 ^ n⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n)
      (summable_pow_mul_geometric_of_norm_lt_one 1 hr)hr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)hsummR:Summable fun n ↦ ↑n.divisors.card / 2 ^ n⊢ ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n
  -- Bridge `ℕ+` to `ℕ`: the `n = 0` term is `0` on both sides.
  rw [← (tsum_zero_pnat_eq_tsum_nat hsummL),hr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)hsummR:Summable fun n ↦ ↑n.divisors.card / 2 ^ n⊢ 1 / (2 ^ 0 - 1) + ∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ nhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)hsummR:Summable fun n ↦ ↑n.divisors.card / 2 ^ n⊢ 1 / (2 ^ 0 - 1) + ∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) =
  ↑(Nat.divisors 0).card / 2 ^ 0 + ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑n ← (tsum_zero_pnat_eq_tsum_nat hsummR)hr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)hsummR:Summable fun n ↦ ↑n.divisors.card / 2 ^ n⊢ 1 / (2 ^ 0 - 1) + ∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) =
  ↑(Nat.divisors 0).card / 2 ^ 0 + ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)hsummR:Summable fun n ↦ ↑n.divisors.card / 2 ^ n⊢ 1 / (2 ^ 0 - 1) + ∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) =
  ↑(Nat.divisors 0).card / 2 ^ 0 + ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑n]hr:‖1 / 2‖ < 1hpos:∀ (n : ℕ), 0 < n → 2 ≤ 2 ^ nkey:∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑nhsummL:Summable fun n ↦ 1 / (2 ^ n - 1)hsummR:Summable fun n ↦ ↑n.divisors.card / 2 ^ n⊢ 1 / (2 ^ 0 - 1) + ∑' (n : ℕ+), 1 / (2 ^ ↑n - 1) =
  ↑(Nat.divisors 0).card / 2 ^ 0 + ∑' (n : ℕ+), ↑(↑n).divisors.card / 2 ^ ↑n
  simpa using keyAll goals completed! 🐙

Show that $$ \sum_{n} \frac{d(n)}{2^n} $$ is irrational.

[Er48] Erdős, P., On arithmetical properties of Lambert series. J. Indian Math. Soc. (N.S.) (1948), 63-66.

@[category research solved, AMS 11]
theorem erdos_257.variants.tsum_top :
    Irrational <| ∑' n, n.divisors.card / (2 ^ n : ℝ) := by⊢ Irrational (∑' (n : ℕ), ↑n.divisors.card / 2 ^ n)
  sorryAll goals completed! 🐙

end Erdos257