Lambert-series identity for the omega series

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

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. hgeom have ∀ (p : ℕ), (2 : ℕ) ≤ p → ∑' (k : ℕ), ((1 / 2 : ℝ) ^ p) ^ (k + (1 : ℕ)) = (1 : ℝ) / ((2 : ℝ) ^ p - (1 : ℝ))

   Leaves ∑' (n : ℕ), (↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n = ∑' (p : Nat.Primes), (1 : ℝ) / ((2 : ℝ) ^ (↑p : ℕ) - (1 : ℝ)), with hgeom : ∀ (p : ℕ), (2 : ℕ) ≤ p → ∑' (k : ℕ), ((1 / 2 : ℝ) ^ p) ^ (k + (1 : ℕ)) = (1 : ℝ) / ((2 : ℝ) ^ p - (1 : ℝ)).

   Uses library pow_succ, tsum_mul_right, tsum_geometric_of_lt_one, one_div, inv_pow.

   Lean, lines 8–17

     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

   targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, lines 8–17 at a6cbbb25bda6 ↗

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

      Leaves ∑' (k : ℕ), ((1 / 2 : ℝ) ^ p) ^ (k + (1 : ℕ)) = (1 : ℝ) / ((2 : ℝ) ^ p - (1 : ℝ)), with hr0 : (0 : ℝ) ≤ (1 / 2 : ℝ) ^ p.

      Lean, line 11

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

      targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, line 11 at a6cbbb25bda6 ↗

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

      Leaves ∑' (k : ℕ), ((1 / 2 : ℝ) ^ p) ^ (k + (1 : ℕ)) = (1 : ℝ) / ((2 : ℝ) ^ p - (1 : ℝ)), with hr1 : (1 / 2 : ℝ) ^ p < (1 : ℝ).

      Uses library pow_lt_one₀.

      Lean, line 12

          have hr1 : (1 / 2 : ℝ) ^ p < 1 := pow_lt_one₀ (by norm_num) (by norm_num) (by omega)

      targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, line 12 at a6cbbb25bda6 ↗

   3. hgeom.h2 have (1 : ℝ) < (2 : ℝ) ^ p

      Leaves ∑' (k : ℕ), ((1 / 2 : ℝ) ^ p) ^ (k + (1 : ℕ)) = (1 : ℝ) / ((2 : ℝ) ^ p - (1 : ℝ)), with h2 : (1 : ℝ) < (2 : ℝ) ^ p.

      Uses library one_lt_pow₀.

      Lean, line 13

          have h2 : (1 : ℝ) < 2 ^ p := one_lt_pow₀ (by norm_num) (by omega)

      targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, line 13 at a6cbbb25bda6 ↗

   4. hgeom.h3 have (2 : ℝ) ^ p - (1 : ℝ) ≠ (0 : ℝ) routine: linarith

      Leaves ∑' (k : ℕ), ((1 / 2 : ℝ) ^ p) ^ (k + (1 : ℕ)) = (1 : ℝ) / ((2 : ℝ) ^ p - (1 : ℝ)), with h3 : (2 : ℝ) ^ p - (1 : ℝ) ≠ (0 : ℝ).

      Lean, line 14

          have h3 : (2 : ℝ) ^ p - 1 ≠ 0 := by linarith

      targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, line 14 at a6cbbb25bda6 ↗

2. hD have ∀ (p : ℕ), Nat.Prime p → (∑' (n : ℕ), if p ∣ n + (1 : ℕ) then (1 / 2 : ℝ) ^ (n + (1 : ℕ)) else (0 : ℝ)) = ∑' (k : ℕ), ((1 / 2 : ℝ) ^ p) ^ (k + (1 : ℕ))

   Leaves ∑' (n : ℕ), (↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n = ∑' (p : Nat.Primes), (1 : ℝ) / ((2 : ℝ) ^ (↑p : ℕ) - (1 : ℝ)), with hD : ∀ (p : ℕ), Nat.Prime p → (∑' (n : ℕ), if p ∣ n + (1 : ℕ) then (1 / 2 : ℝ) ^ (n + (1 : ℕ)) else (0 : ℝ)) = ∑' (k : ℕ), ((1 / 2 : ℝ) ^ p) ^ (k + (1 : ℕ)).

   Uses library tsum_eq_tsum_of_ne_zero_bij.

   Lean, lines 19–47

     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]

   targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, lines 19–47 at a6cbbb25bda6 ↗

   1. hD.hp1 have (1 : ℕ) ≤ p

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

      Lean, line 23

          have hp1 : 1 ≤ p := hp.one_lt.le

      targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, line 23 at a6cbbb25bda6 ↗

   2. hD.hk have ∀ (k : ℕ), p * k + (p - (1 : ℕ)) + (1 : ℕ) = p * (k + (1 : ℕ))

      Leaves (∑' (n : ℕ), if p ∣ n + (1 : ℕ) then (1 / 2 : ℝ) ^ (n + (1 : ℕ)) else (0 : ℝ)) = ∑' (k : ℕ), ((1 / 2 : ℝ) ^ p) ^ (k + (1 : ℕ)), with hk : ∀ (k : ℕ), p * k + (p - (1 : ℕ)) + (1 : ℕ) = p * (k + (1 : ℕ)).

      Uses library Nat.mul_succ, Nat.add_assoc, Nat.sub_add_cancel.

      Lean, lines 24–26

          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]

      targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, lines 24–26 at a6cbbb25bda6 ↗

   3. hD.hg have ∀ (k : ℕ), ((1 / 2 : ℝ) ^ p) ^ (k + (1 : ℕ)) ≠ (0 : ℝ)

      Leaves (∑' (n : ℕ), if p ∣ n + (1 : ℕ) then (1 / 2 : ℝ) ^ (n + (1 : ℕ)) else (0 : ℝ)) = ∑' (k : ℕ), ((1 / 2 : ℝ) ^ p) ^ (k + (1 : ℕ)), with hg : ∀ (k : ℕ), ((1 / 2 : ℝ) ^ p) ^ (k + (1 : ℕ)) ≠ (0 : ℝ).

      Lean, line 27

          have hg : ∀ k : ℕ, ((1 / 2 : ℝ) ^ p) ^ (k + 1) ≠ 0 := fun k => by positivity

      targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, line 27 at a6cbbb25bda6 ↗

   4. hD.s4 case

      Leaves Function.Injective fun (k : (↑(Function.support fun (k : ℕ) => ((1 / 2 : ℝ) ^ p) ^ (k + (1 : ℕ))) : Type)) => p * (↑k : ℕ) + (p - (1 : ℕ)).

      Uses library Subtype.ext, Nat.eq_of_mul_eq_mul_left, Nat.add_right_cancel.

      Lean, lines 29–31

          · 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'))

      targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, lines 29–31 at a6cbbb25bda6 ↗

      1. hD.s4.h' have p * (↑k : ℕ) + (p - (1 : ℕ)) = p * (↑k' : ℕ) + (p - (1 : ℕ))

         Leaves k = k', with h' : p * (↑k : ℕ) + (p - (1 : ℕ)) = p * (↑k' : ℕ) + (p - (1 : ℕ)).

         Lean, line 30

               have h' : p * k.1 + (p - 1) = p * k'.1 + (p - 1) := h

         targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, line 30 at a6cbbb25bda6 ↗

   5. hD.s5 case

      Leaves (Function.support fun (n : ℕ) => if p ∣ n + (1 : ℕ) then (1 / 2 : ℝ) ^ (n + (1 : ℕ)) else (0 : ℝ)) ⊆ Set.range fun (k : (↑(Function.support fun (k : ℕ) => ((1 / 2 : ℝ) ^ p) ^ (k + (1 : ℕ))) : Type)) => p * (↑k : ℕ) + (p - (1 : ℕ)).

      Lean, lines 32–43

          · 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

      targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, lines 32–43 at a6cbbb25bda6 ↗

      1. hD.s5.hn' have (if p ∣ n + (1 : ℕ) then (1 / 2 : ℝ) ^ (n + (1 : ℕ)) else (0 : ℝ)) ≠ (0 : ℝ)

         Leaves n ∈ Set.range fun (k : (↑(Function.support fun (k : ℕ) => ((1 / 2 : ℝ) ^ p) ^ (k + (1 : ℕ))) : Type)) => p * (↑k : ℕ) + (p - (1 : ℕ)), with hn' : (if p ∣ n + (1 : ℕ) then (1 / 2 : ℝ) ^ (n + (1 : ℕ)) else (0 : ℝ)) ≠ (0 : ℝ).

         Uses library Function.mem_support.

         Lean, line 33

               have hn' := Function.mem_support.1 hn

         targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, line 33 at a6cbbb25bda6 ↗

      2. hD.s5.hdvd have p ∣ n + (1 : ℕ)

         Leaves n ∈ Set.range fun (k : (↑(Function.support fun (k : ℕ) => ((1 / 2 : ℝ) ^ p) ^ (k + (1 : ℕ))) : Type)) => p * (↑k : ℕ) + (p - (1 : ℕ)), with hdvd : p ∣ n + (1 : ℕ).

         Uses library if_neg.

         Lean, lines 34–36

               have hdvd : p ∣ n + 1 := by
                 by_contra hnot
                 exact hn' (if_neg hnot)

         targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, lines 34–36 at a6cbbb25bda6 ↗

      3. hD.s5.s3 obtain p ∣ n + (1 : ℕ)

         Leaves n ∈ Set.range fun (k : (↑(Function.support fun (k : ℕ) => ((1 / 2 : ℝ) ^ p) ^ (k + (1 : ℕ))) : Type)) => p * (↑k : ℕ) + (p - (1 : ℕ)), with m : ℕ, hm : n + (1 : ℕ) = p * m.

         Lean, line 37

               obtain ⟨m, hm⟩ := hdvd

         targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, line 37 at a6cbbb25bda6 ↗

      4. hD.s5.s4 case routine: omega

         Leaves n ∈ Set.range fun (k : (↑(Function.support fun (k : ℕ) => ((1 / 2 : ℝ) ^ p) ^ (k + (1 : ℕ))) : Type)) => p * (↑k : ℕ) + (p - (1 : ℕ)).

         Lean, line 39

               · omega

         targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, line 39 at a6cbbb25bda6 ↗

      5. hD.s5.s5 case

         Leaves n ∈ Set.range fun (k : (↑(Function.support fun (k : ℕ) => ((1 / 2 : ℝ) ^ p) ^ (k + (1 : ℕ))) : Type)) => p * (↑k : ℕ) + (p - (1 : ℕ)).

         Uses library Exists.intro Existential introduction. , Subtype.mk, Nat.add_right_cancel.

         Lean, lines 40–43

               · refine ⟨⟨k, hg k⟩, ?_⟩
                 show p * k + (p - 1) = n
                 rw [← hk k] at hm
                 exact (Nat.add_right_cancel hm).symm

         targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, lines 40–43 at a6cbbb25bda6 ↗

   6. hD.s6 case

      Leaves ∀ (x : (↑(Function.support fun (k : ℕ) => ((1 / 2 : ℝ) ^ p) ^ (k + (1 : ℕ))) : Type)), (if p ∣ p * (↑x : ℕ) + (p - (1 : ℕ)) + (1 : ℕ) then (1 / 2 : ℝ) ^ (p * (↑x : ℕ) + (p - (1 : ℕ)) + (1 : ℕ)) else (0 : ℝ)) = ((1 / 2 : ℝ) ^ p) ^ ((↑x : ℕ) + (1 : ℕ)).

      Uses library if_pos, dvd_mul_right, pow_mul.

      Lean, lines 44–47

          · 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]

      targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, lines 44–47 at a6cbbb25bda6 ↗

3. hcol have ∀ (p : Nat.Primes), (∑' (n : ℕ), if (↑p : ℕ) ∣ n + (1 : ℕ) then (1 / 2 : ℝ) ^ (n + (1 : ℕ)) else (0 : ℝ)) = (1 : ℝ) / ((2 : ℝ) ^ (↑p : ℕ) - (1 : ℝ))

   Leaves ∑' (n : ℕ), (↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n = ∑' (p : Nat.Primes), (1 : ℝ) / ((2 : ℝ) ^ (↑p : ℕ) - (1 : ℝ)), with hcol : ∀ (p : Nat.Primes), (∑' (n : ℕ), if (↑p : ℕ) ∣ n + (1 : ℕ) then (1 / 2 : ℝ) ^ (n + (1 : ℕ)) else (0 : ℝ)) = (1 : ℝ) / ((2 : ℝ) ^ (↑p : ℕ) - (1 : ℝ)).

   Uses library Nat.Primes The type of prime numbers .

   Lean, lines 49–53

     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]

   targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, lines 49–53 at a6cbbb25bda6 ↗

4. hR have ∀ (p : ℕ), Summable fun (n : ℕ) => if p ∣ n + (1 : ℕ) then (1 / 2 : ℝ) ^ (n + (1 : ℕ)) else (0 : ℝ)

   Leaves ∑' (n : ℕ), (↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n = ∑' (p : Nat.Primes), (1 : ℝ) / ((2 : ℝ) ^ (↑p : ℕ) - (1 : ℝ)), with hR : ∀ (p : ℕ), Summable fun (n : ℕ) => if p ∣ n + (1 : ℕ) then (1 / 2 : ℝ) ^ (n + (1 : ℕ)) else (0 : ℝ).

   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. , summable_geometric_of_lt_one.

   Lean, lines 55–62

     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

   targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, lines 55–62 at a6cbbb25bda6 ↗

   1. hR.s1 case

      Leaves (0 : ℝ) ≤ if p ∣ n + (1 : ℕ) then (1 / 2 : ℝ) ^ (n + (1 : ℕ)) else (0 : ℝ).

      Lean, line 59

          · split_ifs <;> positivity

      targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, line 59 at a6cbbb25bda6 ↗

   2. hR.s2 case

      Leaves (if p ∣ n + (1 : ℕ) then (1 / 2 : ℝ) ^ (n + (1 : ℕ)) else (0 : ℝ)) ≤ (1 / 2 : ℝ) ^ n.

      Lean, lines 60–62

          · split_ifs
            · exact pow_le_pow_of_le_one (by norm_num) (by norm_num) (Nat.le_succ n)
            · positivity

      targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, lines 60–62 at a6cbbb25bda6 ↗

      1. hR.s2.s1 case

         Leaves (1 / 2 : ℝ) ^ (n + (1 : ℕ)) ≤ (1 / 2 : ℝ) ^ n.

         Uses library pow_le_pow_of_le_one, Nat.le_succ.

         Lean, line 61

               · exact pow_le_pow_of_le_one (by norm_num) (by norm_num) (Nat.le_succ n)

         targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, line 61 at a6cbbb25bda6 ↗

      2. hR.s2.s2 case routine: positivity

         Leaves (0 : ℝ) ≤ (1 / 2 : ℝ) ^ n.

         Lean, line 62

               · positivity

         targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, line 62 at a6cbbb25bda6 ↗

5. hb have ∀ (p : ℕ), Nat.Prime p → (1 : ℝ) / ((2 : ℝ) ^ p - (1 : ℝ)) ≤ (2 : ℝ) * (1 / 2 : ℝ) ^ p

   Leaves ∑' (n : ℕ), (↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n = ∑' (p : Nat.Primes), (1 : ℝ) / ((2 : ℝ) ^ (↑p : ℕ) - (1 : ℝ)), with hb : ∀ (p : ℕ), Nat.Prime p → (1 : ℝ) / ((2 : ℝ) ^ p - (1 : ℝ)) ≤ (2 : ℝ) * (1 / 2 : ℝ) ^ p.

   Lean, lines 64–71

     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]

   targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, lines 64–71 at a6cbbb25bda6 ↗

   1. hb.h2p have (2 : ℝ) ≤ (2 : ℝ) ^ p

      Leaves (1 : ℝ) / ((2 : ℝ) ^ p - (1 : ℝ)) ≤ (2 : ℝ) * (1 / 2 : ℝ) ^ p, with h2p : (2 : ℝ) ≤ (2 : ℝ) ^ p.

      Lean, lines 66–68

          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

      targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, lines 66–68 at a6cbbb25bda6 ↗

      1. hb.h2p.s1 calc (2 : ℝ) = (2 : ℝ) ^ (1 : ℕ)

         Closes the goal.

         Uses library pow_one.

         Lean, line 67

               calc (2 : ℝ) = 2 ^ 1 := (pow_one 2).symm

         targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, line 67 at a6cbbb25bda6 ↗

      2. hb.h2p.s2 calc (2 : ℝ) ^ (1 : ℕ) ≤ (2 : ℝ) ^ p

         Closes the goal.

         Uses library pow_le_pow_right₀.

         Lean, line 68

                 _ ≤ 2 ^ p := pow_le_pow_right₀ (by norm_num) hp.one_lt.le

         targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, line 68 at a6cbbb25bda6 ↗

   2. hb.hpos have (0 : ℝ) < (2 : ℝ) ^ p / (2 : ℝ) routine: positivity

      Leaves (1 : ℝ) / ((2 : ℝ) ^ p - (1 : ℝ)) ≤ (2 : ℝ) * (1 / 2 : ℝ) ^ p, with hpos : (0 : ℝ) < (2 : ℝ) ^ p / (2 : ℝ).

      Lean, line 69

          have hpos : (0 : ℝ) < 2 ^ p / 2 := by positivity

      targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, line 69 at a6cbbb25bda6 ↗

   3. hb.s3 calc (1 : ℝ) / ((2 : ℝ) ^ p - (1 : ℝ)) ≤ (1 : ℝ) / ((2 : ℝ) ^ p / (2 : ℝ))

      Closes the goal.

      Uses library one_div_le_one_div_of_le.

      Lean, line 70

          calc (1 : ℝ) / (2 ^ p - 1) ≤ 1 / (2 ^ p / 2) := one_div_le_one_div_of_le hpos (by linarith)

      targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, line 70 at a6cbbb25bda6 ↗

   4. hb.s4 calc

      Closes the goal.

      Uses library one_div_div, one_div_pow, mul_one_div.

      Lean, line 71

            _ = 2 * (1 / 2 : ℝ) ^ p := by rw [one_div_div, one_div_pow, mul_one_div]

      targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, line 71 at a6cbbb25bda6 ↗

6. hSc have Summable fun (p : Nat.Primes) => (1 : ℝ) / ((2 : ℝ) ^ (↑p : ℕ) - (1 : ℝ))

   Leaves ∑' (n : ℕ), (↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n = ∑' (p : Nat.Primes), (1 : ℝ) / ((2 : ℝ) ^ (↑p : ℕ) - (1 : ℝ)), with hSc : Summable fun (p : Nat.Primes) => (1 : ℝ) / ((2 : ℝ) ^ (↑p : ℕ) - (1 : ℝ)).

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

   Lean, lines 72–78

     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

   targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, lines 72–78 at a6cbbb25bda6 ↗

   1. hSc.hg have Summable fun (n : ℕ) => (2 : ℝ) * (1 / 2 : ℝ) ^ n

      Leaves Summable fun (p : Nat.Primes) => (1 : ℝ) / ((2 : ℝ) ^ (↑p : ℕ) - (1 : ℝ)), with hg : Summable fun (n : ℕ) => (2 : ℝ) * (1 / 2 : ℝ) ^ n.

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

      Lean, lines 73–74

          have hg : Summable (fun n : ℕ => 2 * (1 / 2 : ℝ) ^ n) :=
            (summable_geometric_of_lt_one (by norm_num) (by norm_num)).mul_left 2

      targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, lines 73–74 at a6cbbb25bda6 ↗

   2. hSc.s2 case

      Leaves (0 : ℝ) ≤ (1 : ℝ) / ((2 : ℝ) ^ (↑p : ℕ) - (1 : ℝ)).

      Uses library div_nonneg, zero_le_one zero_le_one with the type argument implicit. .

      Lean, lines 76–77

          · have : (1 : ℝ) < 2 ^ (p : ℕ) := one_lt_pow₀ (by norm_num) p.2.ne_zero
            exact div_nonneg zero_le_one (by linarith)

      targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, lines 76–77 at a6cbbb25bda6 ↗

      1. hSc.s2.this have (1 : ℝ) < (2 : ℝ) ^ (↑p : ℕ)

         Leaves (0 : ℝ) ≤ (1 : ℝ) / ((2 : ℝ) ^ (↑p : ℕ) - (1 : ℝ)), with this : (1 : ℝ) < (2 : ℝ) ^ (↑p : ℕ).

         Uses library one_lt_pow₀.

         Lean, line 76

             · have : (1 : ℝ) < 2 ^ (p : ℕ) := one_lt_pow₀ (by norm_num) p.2.ne_zero

         targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, line 76 at a6cbbb25bda6 ↗

   3. hSc.s3 case

      Leaves (1 : ℝ) / ((2 : ℝ) ^ (↑p : ℕ) - (1 : ℝ)) ≤ ((fun (n : ℕ) => (2 : ℝ) * (1 / 2 : ℝ) ^ n) ∘ Subtype.val) p.

      Lean, line 78

          · exact hb p p.2

      targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, line 78 at a6cbbb25bda6 ↗

7. hC have Summable (Function.uncurry fun (p : Nat.Primes) (n : ℕ) => if (↑p : ℕ) ∣ n + (1 : ℕ) then (1 / 2 : ℝ) ^ (n + (1 : ℕ)) else (0 : ℝ))

   Leaves ∑' (n : ℕ), (↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n = ∑' (p : Nat.Primes), (1 : ℝ) / ((2 : ℝ) ^ (↑p : ℕ) - (1 : ℝ)), with hC : Summable (Function.uncurry fun (p : Nat.Primes) (n : ℕ) => if (↑p : ℕ) ∣ n + (1 : ℕ) then (1 / 2 : ℝ) ^ (n + (1 : ℕ)) else (0 : ℝ)).

   Uses library Summable Summable f means that f has some (infinite) sum with respect to L. , Function.uncurry Transforms a two-parameter function into an equivalent function from pairs. , Nat.Primes The type of prime numbers , summable_prod_of_nonneg, And.intro And.intro : a → b → a ∧ b is the constructor for the And operation. .

   Lean, lines 80–88

     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)

   targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, lines 80–88 at a6cbbb25bda6 ↗

   1. hC.hnn have (0 : Nat.Primes × ℕ → ℝ) ≤ Function.uncurry fun (p : Nat.Primes) (n : ℕ) => if (↑p : ℕ) ∣ n + (1 : ℕ) then (1 / 2 : ℝ) ^ (n + (1 : ℕ)) else (0 : ℝ)

      Leaves Summable (Function.uncurry fun (p : Nat.Primes) (n : ℕ) => if (↑p : ℕ) ∣ n + (1 : ℕ) then (1 / 2 : ℝ) ^ (n + (1 : ℕ)) else (0 : ℝ)), with hnn : (0 : Nat.Primes × ℕ → ℝ) ≤ Function.uncurry fun (p : Nat.Primes) (n : ℕ) => if (↑p : ℕ) ∣ n + (1 : ℕ) then (1 / 2 : ℝ) ^ (n + (1 : ℕ)) else (0 : ℝ).

      Uses library Nat.Primes The type of prime numbers , Function.uncurry Transforms a two-parameter function into an equivalent function from pairs. .

      Lean, lines 82–86

          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

      targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, lines 82–86 at a6cbbb25bda6 ↗

8. hswap have (∑' (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 : ℝ)

   Leaves ∑' (n : ℕ), (↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n = ∑' (p : Nat.Primes), (1 : ℝ) / ((2 : ℝ) ^ (↑p : ℕ) - (1 : ℝ)), with 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 : ℝ).

   Uses library Nat.Primes The type of prime numbers .

   Lean, lines 90–92

     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

   targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, lines 90–92 at a6cbbb25bda6 ↗

9. hBgen have ∀ (m : ℕ), m ≠ (0 : ℕ) → ∀ (c : ℝ), (∑' (p : Nat.Primes), if (↑p : ℕ) ∣ m then c else (0 : ℝ)) = (↑((ω : ℕ → ℕ) m) : ℝ) * c

   Leaves ∑' (n : ℕ), (↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n = ∑' (p : Nat.Primes), (1 : ℝ) / ((2 : ℝ) ^ (↑p : ℕ) - (1 : ℝ)), with hBgen : ∀ (m : ℕ), m ≠ (0 : ℕ) → ∀ (c : ℝ), (∑' (p : Nat.Primes), if (↑p : ℕ) ∣ m then c else (0 : ℝ)) = (↑((ω : ℕ → ℕ) m) : ℝ) * c.

   Uses library Nat.Primes The type of prime numbers , Finset Finset α is the type of finite sets of elements of α. , Function.Embedding.mk, Subtype.mk, Nat.mem_primeFactors, Subtype.ext, Subtype.mk.inj, tsum_eq_sum, Finset.sum_ite_of_true, Finset.sum_const, nsmul_eq_mul.

   Lean, lines 94–121

     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ω]

   targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, lines 94–121 at a6cbbb25bda6 ↗

   1. hBgen.hmem have ∀ (p : Nat.Primes), p ∈ S ↔ (↑p : ℕ) ∈ m.primeFactors

      Leaves (∑' (p : Nat.Primes), if (↑p : ℕ) ∣ m then c else (0 : ℝ)) = (↑((ω : ℕ → ℕ) m) : ℝ) * c, with hmem : ∀ (p : Nat.Primes), p ∈ S ↔ (↑p : ℕ) ∈ m.primeFactors.

      Uses library Nat.Primes The type of prime numbers .

      Lean, lines 100–107

          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⟩

      targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, lines 100–107 at a6cbbb25bda6 ↗

      1. hBgen.hmem.s1 case

         Leaves p ∈ S → (↑p : ℕ) ∈ m.primeFactors.

         Lean, lines 103–105

               · intro hp
                 obtain ⟨q, -, rfl⟩ := Finset.mem_map.1 hp
                 exact q.2

         targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, lines 103–105 at a6cbbb25bda6 ↗

         1. hBgen.hmem.s1.s1 obtain printed form did not read back: shown as its Lean lines only

                    obtain ⟨q, -, rfl⟩ := Finset.mem_map.1 hp

            targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, line 104 at a6cbbb25bda6 ↗

      2. hBgen.hmem.s2 case

         Leaves (↑p : ℕ) ∈ m.primeFactors → p ∈ S.

         Uses library Finset.mem_map, Exists.intro Existential introduction. , Subtype.mk, Finset.mem_attach, Subtype.ext, rfl rfl : a = a is the unique constructor of the equality type. .

         Lean, lines 106–107

               · intro hp
                 exact Finset.mem_map.2 ⟨⟨p.1, hp⟩, Finset.mem_attach _ _, Subtype.ext rfl⟩

         targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, lines 106–107 at a6cbbb25bda6 ↗

   2. hBgen.hfin have ∀ p ∉ S, (if (↑p : ℕ) ∣ m then c else (0 : ℝ)) = (0 : ℝ)

      Leaves (∑' (p : Nat.Primes), if (↑p : ℕ) ∣ m then c else (0 : ℝ)) = (↑((ω : ℕ → ℕ) m) : ℝ) * c, with hfin : ∀ p ∉ S, (if (↑p : ℕ) ∣ m then c else (0 : ℝ)) = (0 : ℝ).

      Uses library Nat.Primes The type of prime numbers , if_neg, Nat.mem_primeFactors, And.intro And.intro : a → b → a ∧ b is the constructor for the And operation. .

      Lean, lines 108–112

          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⟩))

      targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, lines 108–112 at a6cbbb25bda6 ↗

   3. hBgen.hcard have S.card = m.primeFactors.card routine: simp

      Leaves (↑S.card : ℝ) * c = (↑((ω : ℕ → ℕ) m) : ℝ) * c, with hcard : S.card = m.primeFactors.card.

      Uses library Finset.card_map, Finset.card_attach.

      Lean, lines 116–117

          have hcard : S.card = m.primeFactors.card := by
            simp [S, Finset.card_map, Finset.card_attach]

      targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, lines 116–117 at a6cbbb25bda6 ↗

   4. hBgen.h_x3c9 (hω) have (↑m.primeFactors.card : ℝ) = (↑((ω : ℕ → ℕ) m) : ℝ)

      Leaves (↑S.card : ℝ) * c = (↑((ω : ℕ → ℕ) m) : ℝ) * c, with hω : (↑m.primeFactors.card : ℝ) = (↑((ω : ℕ → ℕ) m) : ℝ).

      Uses library ArithmeticFunction.cardDistinctFactors_apply.

      Lean, lines 118–120

          have hω : (m.primeFactors.card : ℝ) = ω m := by
            simp [ArithmeticFunction.cardDistinctFactors_apply]
            rfl

      targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, lines 118–120 at a6cbbb25bda6 ↗

10. hB have ∀ (n : ℕ), (∑' (p : Nat.Primes), if (↑p : ℕ) ∣ n + (1 : ℕ) then (1 / 2 : ℝ) ^ (n + (1 : ℕ)) else (0 : ℝ)) = (↑((ω : ℕ → ℕ) (n + (1 : ℕ))) : ℝ) / (2 : ℝ) ^ (n + (1 : ℕ))

    Leaves ∑' (n : ℕ), (↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n = ∑' (p : Nat.Primes), (1 : ℝ) / ((2 : ℝ) ^ (↑p : ℕ) - (1 : ℝ)), with hB : ∀ (n : ℕ), (∑' (p : Nat.Primes), if (↑p : ℕ) ∣ n + (1 : ℕ) then (1 / 2 : ℝ) ^ (n + (1 : ℕ)) else (0 : ℝ)) = (↑((ω : ℕ → ℕ) (n + (1 : ℕ))) : ℝ) / (2 : ℝ) ^ (n + (1 : ℕ)).

    Uses library Nat.Primes The type of prime numbers , one_div_pow, mul_one_div.

    Lean, lines 122–126

      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]

    targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, lines 122–126 at a6cbbb25bda6 ↗

11. hbound have ∀ (n : ℕ), (↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n ≤ (↑n : ℝ) ^ (1 : ℕ) * (1 / 2 : ℝ) ^ n + (1 / 2 : ℝ) ^ n

    Leaves ∑' (n : ℕ), (↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n = ∑' (p : Nat.Primes), (1 : ℝ) / ((2 : ℝ) ^ (↑p : ℕ) - (1 : ℝ)), with hbound : ∀ (n : ℕ), (↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n ≤ (↑n : ℝ) ^ (1 : ℕ) * (1 / 2 : ℝ) ^ n + (1 / 2 : ℝ) ^ n.

    Uses library pow_one, one_div, inv_pow, div_eq_mul_inv Dividing by an element is the same as multiplying by its inverse. , mul_le_mul_of_nonneg_right.

    Lean, lines 128–141

      have hbound : ∀ n : ℕ,
          (ω n : ℝ) / 2 ^ n ≤ (n : ℝ) ^ 1 * (1 / 2 : ℝ) ^ n + (1 / 2 : ℝ) ^ n := by
        intro n
        have h1 : ω n ≤ n + 1 := by
          rw [ArithmeticFunction.cardDistinctFactors_apply]
          calc n.primeFactorsList.dedup.length = n.primeFactors.card := rfl
            _ ≤ (Finset.range (n + 1)).card :=
                Finset.card_le_card (fun p hp =>
                  Finset.mem_range.2 (Nat.lt_succ_of_le (Nat.le_of_mem_primeFactors hp)))
            _ = n + 1 := Finset.card_range _
        have h2 : (ω n : ℝ) ≤ (n : ℝ) + 1 := by exact_mod_cast h1
        have h4 : (0 : ℝ) ≤ ((2 : ℝ) ^ n)⁻¹ := by positivity
        rw [pow_one, one_div, inv_pow, div_eq_mul_inv]
        nlinarith [mul_le_mul_of_nonneg_right h2 h4]

    targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, lines 128–141 at a6cbbb25bda6 ↗

    1. hbound.h1 have (ω : ℕ → ℕ) n ≤ n + (1 : ℕ)

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

       Uses library ArithmeticFunction.cardDistinctFactors_apply.

       Lean, lines 131–137

           have h1 : ω n ≤ n + 1 := by
             rw [ArithmeticFunction.cardDistinctFactors_apply]
             calc n.primeFactorsList.dedup.length = n.primeFactors.card := rfl
               _ ≤ (Finset.range (n + 1)).card :=
                   Finset.card_le_card (fun p hp =>
                     Finset.mem_range.2 (Nat.lt_succ_of_le (Nat.le_of_mem_primeFactors hp)))
               _ = n + 1 := Finset.card_range _

       targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, lines 131–137 at a6cbbb25bda6 ↗

       1. hbound.h1.s1 calc n.primeFactorsList.dedup.length = n.primeFactors.card

          Closes the goal.

          Uses library rfl rfl : a = a is the unique constructor of the equality type. .

          Lean, line 133

                calc n.primeFactorsList.dedup.length = n.primeFactors.card := rfl

          targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, line 133 at a6cbbb25bda6 ↗

       2. hbound.h1.s2 calc n.primeFactors.card ≤ (Finset.range (n + (1 : ℕ))).card

          Closes the goal.

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

          Lean, lines 134–136

                  _ ≤ (Finset.range (n + 1)).card :=
                      Finset.card_le_card (fun p hp =>
                        Finset.mem_range.2 (Nat.lt_succ_of_le (Nat.le_of_mem_primeFactors hp)))

          targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, lines 134–136 at a6cbbb25bda6 ↗

       3. hbound.h1.s3 calc (Finset.range (n + (1 : ℕ))).card = n + (1 : ℕ)

          Closes the goal.

          Uses library Finset.card_range.

          Lean, line 137

                  _ = n + 1 := Finset.card_range _

          targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, line 137 at a6cbbb25bda6 ↗

    2. hbound.h2 have (↑((ω : ℕ → ℕ) n) : ℝ) ≤ (↑n : ℝ) + (1 : ℝ)

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

       Lean, line 138

           have h2 : (ω n : ℝ) ≤ (n : ℝ) + 1 := by exact_mod_cast h1

       targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, line 138 at a6cbbb25bda6 ↗

    3. hbound.h4 have (0 : ℝ) ≤ ((2 : ℝ) ^ n)⁻¹ routine: positivity

       Leaves (↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n ≤ (↑n : ℝ) ^ (1 : ℕ) * (1 / 2 : ℝ) ^ n + (1 / 2 : ℝ) ^ n, with h4 : (0 : ℝ) ≤ ((2 : ℝ) ^ n)⁻¹.

       Lean, line 139

           have h4 : (0 : ℝ) ≤ ((2 : ℝ) ^ n)⁻¹ := by positivity

       targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, line 139 at a6cbbb25bda6 ↗

12. hsum have Summable fun (n : ℕ) => (↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n

    Leaves ∑' (n : ℕ), (↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n = ∑' (p : Nat.Primes), (1 : ℝ) / ((2 : ℝ) ^ (↑p : ℕ) - (1 : ℝ)), with hsum : Summable fun (n : ℕ) => (↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n.

    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. , summable_pow_mul_geometric_of_norm_lt_one, Real.norm_eq_abs, summable_geometric_of_lt_one.

    Lean, lines 142–145

      have hsum : Summable (fun n : ℕ => (ω n : ℝ) / 2 ^ n) := by
        refine Summable.of_nonneg_of_le (fun n => by positivity) hbound ?_
        exact (summable_pow_mul_geometric_of_norm_lt_one 1 (by norm_num [Real.norm_eq_abs])).add
          (summable_geometric_of_lt_one (by norm_num) (by norm_num))

    targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, lines 142–145 at a6cbbb25bda6 ↗

13. s13 calc ∑' (n : ℕ), (↑((ω : ℕ → ℕ) n) : ℝ) / (2 : ℝ) ^ n = ∑' (n : ℕ), (↑((ω : ℕ → ℕ) (n + (1 : ℕ))) : ℝ) / (2 : ℝ) ^ (n + (1 : ℕ))

    Closes the goal.

    Lean, lines 147–150

      calc ∑' n : ℕ, (ω n : ℝ) / 2 ^ n
          = ∑' n : ℕ, (ω (n + 1) : ℝ) / 2 ^ (n + 1) := by
            rw [hsum.tsum_eq_zero_add]
            simp

    targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, lines 147–150 at a6cbbb25bda6 ↗

14. s14 calc ∑' (n : ℕ), (↑((ω : ℕ → ℕ) (n + (1 : ℕ))) : ℝ) / (2 : ℝ) ^ (n + (1 : ℕ)) = ∑' (n : ℕ) (p : Nat.Primes), if (↑p : ℕ) ∣ n + (1 : ℕ) then (1 / 2 : ℝ) ^ (n + (1 : ℕ)) else (0 : ℝ)

    Closes the goal.

    Uses library Nat.Primes The type of prime numbers , tsum_congr.

    Lean, lines 151–152

        _ = ∑' n : ℕ, ∑' p : Nat.Primes, (if (p : ℕ) ∣ n + 1 then (1 / 2 : ℝ) ^ (n + 1) else 0) :=
            tsum_congr (fun n => (hB n).symm)

    targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, lines 151–152 at a6cbbb25bda6 ↗

15. s15 calc (∑' (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 : ℝ)

    Closes the goal.

    Uses library Nat.Primes The type of prime numbers .

    Lean, line 153

        _ = ∑' p : Nat.Primes, ∑' n : ℕ, (if (p : ℕ) ∣ n + 1 then (1 / 2 : ℝ) ^ (n + 1) else 0) := hswap

    targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, line 153 at a6cbbb25bda6 ↗

16. s16 calc (∑' (p : Nat.Primes) (n : ℕ), if (↑p : ℕ) ∣ n + (1 : ℕ) then (1 / 2 : ℝ) ^ (n + (1 : ℕ)) else (0 : ℝ)) = ∑' (p : Nat.Primes), (1 : ℝ) / ((2 : ℝ) ^ (↑p : ℕ) - (1 : ℝ))

    Closes the goal.

    Uses library Nat.Primes The type of prime numbers , tsum_congr.

    Lean, line 154

        _ = ∑' p : Nat.Primes, (1 : ℝ) / (2 ^ (p : ℕ) - 1) := tsum_congr hcol

    targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean, line 154 at a6cbbb25bda6 ↗