1. FormalConjectures
  2. ErdosProblems
  3. «158»
/- Copyright 2026 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 158

References:

    erdosproblems.com/158

    [ESS94] Erdős, P. and Sárközy, A. and Sós, T., On Sum Sets of Sidon Sets, I. Journal of Number Theory (1994), 329-347.

open Filter Real namespace Erdos158

A set A ⊆ ℕ is said to be a B₂[g] set if for all n, the equation a + a' = n, a ≤ a', a, a' ∈ A has at most g solutions. This is defined in [ESS94].

def B2 (g : ℕ) (A : Set ℕ) : Prop := ∀ n, {x : ℕ × ℕ | x.1 + x.2 = n ∧ x.1 ≤ x.2 ∧ x.1 ∈ A ∧ x.2 ∈ A}.encard ≤ g

A set is B₂[1] iff it is Sidon.

@[category API, AMS 5, simp] lemma b2_one {A : Set ℕ} : B2 1 A ↔ IsSidon A where mp hA a₁ ha₁ a₂ ha₂ b₁ hb₁ b₂ hb₂ h := A:Set ℕhA:B2 1 Aa₁:ℕha₁:a₁ ∈ Aa₂:ℕha₂:a₂ ∈ Ab₁:ℕhb₁:b₁ ∈ Ab₂:ℕhb₂:b₂ ∈ Ah:a₁ + b₁ = a₂ + b₂⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂ A:Set ℕhA:B2 1 Aa₁:ℕha₁:a₁ ∈ Aa₂:ℕha₂:a₂ ∈ Ab₁:ℕhb₁:b₁ ∈ Ab₂:ℕhb₂:b₂ ∈ Ah:a₁ + b₁ = a₂ + b₂this:∀ {A : Set ℕ}, B2 1 A → ∀ a₁ ∈ A, ∀ a₂ ∈ A, ∀ b₁ ∈ A, ∀ b₂ ∈ A, a₁ + b₁ = a₂ + b₂ → a₁ ≤ b₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂h₁:¬a₁ ≤ b₁⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂A:Set ℕhA:B2 1 Aa₁:ℕha₁:a₁ ∈ Aa₂:ℕha₂:a₂ ∈ Ab₁:ℕhb₁:b₁ ∈ Ab₂:ℕhb₂:b₂ ∈ Ah:a₁ + b₁ = a₂ + b₂h₁:a₁ ≤ b₁⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂ A:Set ℕhA:B2 1 Aa₁:ℕha₁:a₁ ∈ Aa₂:ℕha₂:a₂ ∈ Ab₁:ℕhb₁:b₁ ∈ Ab₂:ℕhb₂:b₂ ∈ Ah:a₁ + b₁ = a₂ + b₂this:∀ {A : Set ℕ}, B2 1 A → ∀ a₁ ∈ A, ∀ a₂ ∈ A, ∀ b₁ ∈ A, ∀ b₂ ∈ A, a₁ + b₁ = a₂ + b₂ → a₁ ≤ b₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂h₁:¬a₁ ≤ b₁⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂ A:Set ℕhA:B2 1 Aa₁:ℕha₁:a₁ ∈ Aa₂:ℕha₂:a₂ ∈ Ab₁:ℕhb₁:b₁ ∈ Ab₂:ℕhb₂:b₂ ∈ Ah:a₁ + b₁ = a₂ + b₂this✝:∀ {A : Set ℕ}, B2 1 A → ∀ a₁ ∈ A, ∀ a₂ ∈ A, ∀ b₁ ∈ A, ∀ b₂ ∈ A, a₁ + b₁ = a₂ + b₂ → a₁ ≤ b₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂h₁:¬a₁ ≤ b₁this:b₁ + a₁ = a₂ + b₂ → b₁ ≤ a₁ → b₁ = a₂ ∧ a₁ = b₂ ∨ b₁ = b₂ ∧ a₁ = a₂ := this✝ hA b₁ hb₁ a₂ ha₂ a₁ ha₁ b₂ hb₂⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂ All goals completed! 🐙 A:Set ℕhA:B2 1 Aa₁:ℕha₁:a₁ ∈ Aa₂:ℕha₂:a₂ ∈ Ab₁:ℕhb₁:b₁ ∈ Ab₂:ℕhb₂:b₂ ∈ Ah:a₁ + b₁ = a₂ + b₂h₁:a₁ ≤ b₁this:∀ {A : Set ℕ}, B2 1 A → ∀ a₁ ∈ A, ∀ a₂ ∈ A, ∀ b₁ ∈ A, ∀ b₂ ∈ A, a₁ + b₁ = a₂ + b₂ → a₁ ≤ b₁ → a₂ ≤ b₂ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂h₂:¬a₂ ≤ b₂⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂A:Set ℕhA:B2 1 Aa₁:ℕha₁:a₁ ∈ Aa₂:ℕha₂:a₂ ∈ Ab₁:ℕhb₁:b₁ ∈ Ab₂:ℕhb₂:b₂ ∈ Ah:a₁ + b₁ = a₂ + b₂h₁:a₁ ≤ b₁h₂:a₂ ≤ b₂⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂ A:Set ℕhA:B2 1 Aa₁:ℕha₁:a₁ ∈ Aa₂:ℕha₂:a₂ ∈ Ab₁:ℕhb₁:b₁ ∈ Ab₂:ℕhb₂:b₂ ∈ Ah:a₁ + b₁ = a₂ + b₂h₁:a₁ ≤ b₁this:∀ {A : Set ℕ}, B2 1 A → ∀ a₁ ∈ A, ∀ a₂ ∈ A, ∀ b₁ ∈ A, ∀ b₂ ∈ A, a₁ + b₁ = a₂ + b₂ → a₁ ≤ b₁ → a₂ ≤ b₂ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂h₂:¬a₂ ≤ b₂⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂ A:Set ℕhA:B2 1 Aa₁:ℕha₁:a₁ ∈ Aa₂:ℕha₂:a₂ ∈ Ab₁:ℕhb₁:b₁ ∈ Ab₂:ℕhb₂:b₂ ∈ Ah:a₁ + b₁ = a₂ + b₂h₁:a₁ ≤ b₁this✝:∀ {A : Set ℕ}, B2 1 A → ∀ a₁ ∈ A, ∀ a₂ ∈ A, ∀ b₁ ∈ A, ∀ b₂ ∈ A, a₁ + b₁ = a₂ + b₂ → a₁ ≤ b₁ → a₂ ≤ b₂ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂h₂:¬a₂ ≤ b₂this:a₁ + b₁ = b₂ + a₂ → a₁ ≤ b₁ → b₂ ≤ a₂ → a₁ = b₂ ∧ b₁ = a₂ ∨ a₁ = a₂ ∧ b₁ = b₂ := this✝ hA a₁ ha₁ b₂ hb₂ b₁ hb₁ a₂ ha₂⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂ A:Set ℕhA:B2 1 Aa₁:ℕa₂:ℕb₁:ℕb₂:ℕh:a₁ + b₁ = a₂ + b₂h₁:a₁ ≤ b₁this✝:∀ {A : Set ℕ}, B2 1 A → ∀ a₁ ∈ A, ∀ a₂ ∈ A, ∀ b₁ ∈ A, ∀ b₂ ∈ A, a₁ + b₁ = a₂ + b₂ → a₁ ≤ b₁ → a₂ ≤ b₂ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂h₂:¬a₂ ≤ b₂this:a₁ + b₁ = b₂ + a₂ → a₁ ≤ b₁ → b₂ ≤ a₂ → a₁ = b₂ ∧ b₁ = a₂ ∨ a₁ = a₂ ∧ b₁ = b₂ := this✝ hA a₁ ha₁ b₂ hb₂ b₁ hb₁ a₂ ha₂⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂ All goals completed! 🐙 have := Set.encard_le_one_iff.1 (hA (a₁ + b₁)) ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ (A:Set ℕhA:B2 1 Aa₁:ℕha₁:a₁ ∈ Aa₂:ℕha₂:a₂ ∈ Ab₁:ℕhb₁:b₁ ∈ Ab₂:ℕhb₂:b₂ ∈ Ah:a₁ + b₁ = a₂ + b₂h₁:a₁ ≤ b₁h₂:a₂ ≤ b₂⊢ (a₁, b₁) ∈ {x | x.1 + x.2 = a₁ + b₁ ∧ x.1 ≤ x.2 ∧ x.1 ∈ A ∧ x.2 ∈ A} All goals completed! 🐙) (A:Set ℕhA:B2 1 Aa₁:ℕha₁:a₁ ∈ Aa₂:ℕha₂:a₂ ∈ Ab₁:ℕhb₁:b₁ ∈ Ab₂:ℕhb₂:b₂ ∈ Ah:a₁ + b₁ = a₂ + b₂h₁:a₁ ≤ b₁h₂:a₂ ≤ b₂⊢ (a₂, b₂) ∈ {x | x.1 + x.2 = a₁ + b₁ ∧ x.1 ≤ x.2 ∧ x.1 ∈ A ∧ x.2 ∈ A} All goals completed! 🐙) All goals completed! 🐙 mpr hA n := A:Set ℕhA:IsSidon An:ℕ⊢ {x | x.1 + x.2 = n ∧ x.1 ≤ x.2 ∧ x.1 ∈ A ∧ x.2 ∈ A}.encard ≤ ↑1 A:Set ℕhA:IsSidon An:ℕx:ℕ × ℕy:ℕ × ℕx✝¹:x ∈ {x | x.1 + x.2 = n ∧ x.1 ≤ x.2 ∧ x.1 ∈ A ∧ x.2 ∈ A}x✝:y ∈ {x | x.1 + x.2 = n ∧ x.1 ≤ x.2 ∧ x.1 ∈ A ∧ x.2 ∈ A}h:x.1 + x.2 = np:x.1 ≤ x.2q:x.1 ∈ A ∧ x.2 ∈ Ar:y.1 + y.2 = ns:y.1 ≤ y.2t:y.1 ∈ A ∧ y.2 ∈ A⊢ x = y A:Set ℕhA:IsSidon An:ℕx:ℕ × ℕy:ℕ × ℕx✝¹:x ∈ {x | x.1 + x.2 = n ∧ x.1 ≤ x.2 ∧ x.1 ∈ A ∧ x.2 ∈ A}x✝:y ∈ {x | x.1 + x.2 = n ∧ x.1 ≤ x.2 ∧ x.1 ∈ A ∧ x.2 ∈ A}h:x.1 + x.2 = np:x.1 ≤ x.2q:x.1 ∈ A ∧ x.2 ∈ Ar:y.1 + y.2 = ns:y.1 ≤ y.2t:y.1 ∈ A ∧ y.2 ∈ Athis:x.1 = y.1 ∧ x.2 = y.2 ∨ x.1 = y.2 ∧ x.2 = y.1 := hA x.1 q.left y.1 t.left x.2 q.right y.2 t.right (Eq.trans h (Eq.symm r))⊢ x = y All goals completed! 🐙

Let A be an infinite B₂[2] set. Must liminf |A ∩ {1, ..., N}| * N ^ (- 1 / 2) = 0?

@[category research open, AMS 5] theorem declaration uses 'sorry'erdos_158 : answer(sorry) ↔ ∀ A : Set ℕ, A.Infinite → B2 2 A → liminf (fun N : ℕ => (A ∩ .Iio N).ncard * (N : ℝ) ^ (- 1 / 2 : ℝ)) atTop = 0 := ⊢ True ↔ ∀ (A : Set ℕ), A.Infinite → B2 2 A → liminf (fun N => ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2)) atTop = 0 All goals completed! 🐙

Let A be an infinite Sidon set. Then liminf |A ∩ {1, ..., N}| * N ^ (- 1 / 2) * (log N) ^ (1 / 2) < ∞. This is proved in [ESS94].

@[category research solved, AMS 5] theorem declaration uses 'sorry'erdos_158.variants.isSidon' {A : Set ℕ} (hAinf : A.Infinite) (hAsid : IsSidon A) : liminf (fun N ↦ ENNReal.ofReal ((A ∩ .Iio N).ncard * N ^ (- 1 / 2 : ℝ) * log N ^ (1 / 2 : ℝ))) atTop < ⊤ := A:Set ℕhAinf:A.InfinitehAsid:IsSidon A⊢ liminf (fun N => ENNReal.ofReal (↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2) * log ↑N ^ (1 / 2))) atTop < ⊤ All goals completed! 🐙

As a corollary of erdos_158.isSidon', we can prove that liminf |A ∩ {1, ..., N}| * N ^ (- 1 / 2) = 0 for any infinite Sidon set A.

@[category research solved, AMS 5] theorem erdos_158.variants.isSidon {A : Set ℕ} (hAinf : A.Infinite) (hAsid : IsSidon A) : liminf (fun N : ℕ => (A ∩ .Iio N).ncard * (N : ℝ) ^ (- 1 / 2 : ℝ)) atTop = 0 := A:Set ℕhAinf:A.InfinitehAsid:IsSidon A⊢ liminf (fun N => ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2)) atTop = 0 A:Set ℕhAinf:A.InfinitehAsid:IsSidon Athis:liminf (fun N => ENNReal.ofReal (↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2) * log ↑N ^ (1 / 2))) atTop < ⊤ := isSidon' hAinf hAsid⊢ liminf (fun N => ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2)) atTop = 0 A:Set ℕhAinf:A.InfinitehAsid:IsSidon Ah:liminf (fun N => ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2)) atTop ≠ 0⊢ ⊤ ≤ liminf (fun N => ENNReal.ofReal (↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2) * log ↑N ^ (1 / 2))) atTop A:Set ℕhAinf:A.InfinitehAsid:IsSidon Ah:liminf (fun N => ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2)) atTop ≠ 0⊢ Tendsto (fun N => ENNReal.ofReal (↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2) * log ↑N ^ (1 / 2))) atTop (nhds ⊤) A:Set ℕhAinf:A.InfinitehAsid:IsSidon Ah:liminf (fun N => ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2)) atTop ≠ 0⊢ Tendsto (fun N => ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2) * log ↑N ^ (1 / 2)) atTop atTop obtain ⟨c, hc_pos, hc⟩ : ∃ c > (0 : ℝ), ∀ᶠ N in atTop, c ≤ (A ∩ .Iio N).ncard * N ^ (- 1 / 2 : ℝ) := A:Set ℕhAinf:A.InfinitehAsid:IsSidon Ah:liminf (fun N => ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2)) atTop ≠ 0⊢ ∃ c > 0, ∀ᶠ (N : ℕ) in atTop, c ≤ ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2) suffices ∃ a ∈ {a | ∃ c : ℕ, ∀ b ≥ c, a ≤ ↑(A ∩ .Iio b).ncard * (b : ℝ) ^ (-1 / 2 : ℝ)}, 0 < a A:Set ℕhAinf:A.InfinitehAsid:IsSidon Ah:liminf (fun N => ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2)) atTop ≠ 0this:∃ a ∈ {a | ∃ c, ∀ b ≥ c, a ≤ ↑(A ∩ Set.Iio b).ncard * ↑b ^ (-1 / 2)}, 0 < a := ?m.151⊢ ∃ c > 0, ∀ᶠ (N : ℕ) in atTop, c ≤ ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2) All goals completed! 🐙 A:Set ℕhAinf:A.InfinitehAsid:IsSidon Ah:liminf (fun N => ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2)) atTop ≠ 0ha:∀ a ∈ {a | ∃ c, ∀ b ≥ c, a ≤ ↑(A ∩ Set.Iio b).ncard * ↑b ^ (-1 / 2)}, a ≤ 0⊢ False A:Set ℕhAinf:A.InfinitehAsid:IsSidon Aha:∀ a ∈ {a | ∃ c, ∀ b ≥ c, a ≤ ↑(A ∩ Set.Iio b).ncard * ↑b ^ (-1 / 2)}, a ≤ 0h:sSup {a | ∃ a_1, ∀ b ≥ a_1, a ≤ ↑(A ∩ Set.Iio b).ncard * ↑b ^ (-1 / 2)} ≠ 0⊢ False exact h <| le_antisymm (csSup_le ⟨0, 0, fun n hn => A:Set ℕhAinf:A.InfinitehAsid:IsSidon Aha:∀ a ∈ {a | ∃ c, ∀ b ≥ c, a ≤ ↑(A ∩ Set.Iio b).ncard * ↑b ^ (-1 / 2)}, a ≤ 0h:sSup {a | ∃ a_1, ∀ b ≥ a_1, a ≤ ↑(A ∩ Set.Iio b).ncard * ↑b ^ (-1 / 2)} ≠ 0n:ℕhn:n ≥ 0⊢ 0 ≤ ↑(A ∩ Set.Iio n).ncard * ↑n ^ (-1 / 2) All goals completed! 🐙⟩ ha) <| (le_csSup ⟨0, ha⟩ ⟨0, fun n hn => A:Set ℕhAinf:A.InfinitehAsid:IsSidon Aha:∀ a ∈ {a | ∃ c, ∀ b ≥ c, a ≤ ↑(A ∩ Set.Iio b).ncard * ↑b ^ (-1 / 2)}, a ≤ 0h:sSup {a | ∃ a_1, ∀ b ≥ a_1, a ≤ ↑(A ∩ Set.Iio b).ncard * ↑b ^ (-1 / 2)} ≠ 0n:ℕhn:n ≥ 0⊢ 0 ≤ ↑(A ∩ Set.Iio n).ncard * ↑n ^ (-1 / 2) All goals completed! 🐙⟩) A:Set ℕhAinf:A.InfinitehAsid:IsSidon Ah:liminf (fun N => ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2)) atTop ≠ 0c:ℝhc_pos:c > 0hc:∀ᶠ (N : ℕ) in atTop, c ≤ ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2)⊢ (fun N => c * log ↑N ^ (1 / 2)) ≤ᶠ[atTop] fun N => ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2) * log ↑N ^ (1 / 2)A:Set ℕhAinf:A.InfinitehAsid:IsSidon Ah:liminf (fun N => ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2)) atTop ≠ 0c:ℝhc_pos:c > 0hc:∀ᶠ (N : ℕ) in atTop, c ≤ ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2)⊢ Tendsto (fun N => c * log ↑N ^ (1 / 2)) atTop atTop A:Set ℕhAinf:A.InfinitehAsid:IsSidon Ah:liminf (fun N => ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2)) atTop ≠ 0c:ℝhc_pos:c > 0hc:∀ᶠ (N : ℕ) in atTop, c ≤ ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2)⊢ (fun N => c * log ↑N ^ (1 / 2)) ≤ᶠ[atTop] fun N => ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2) * log ↑N ^ (1 / 2) filter_upwards [hc] with n A:Set ℕhAinf:A.InfinitehAsid:IsSidon Ah:liminf (fun N => ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2)) atTop ≠ 0c:ℝhc_pos:c > 0hc:∀ᶠ (N : ℕ) in atTop, c ≤ ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2)n:ℕhn:c ≤ ↑(A ∩ Set.Iio n).ncard * ↑n ^ (-1 / 2)⊢ c * log ↑n ^ (1 / 2) ≤ ↑(A ∩ Set.Iio n).ncard * ↑n ^ (-1 / 2) * log ↑n ^ (1 / 2) grw [hnAll goals completed! 🐙 A:Set ℕhAinf:A.InfinitehAsid:IsSidon Ah:liminf (fun N => ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2)) atTop ≠ 0c:ℝhc_pos:c > 0hc:∀ᶠ (N : ℕ) in atTop, c ≤ ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2)⊢ Tendsto (fun N => c * log ↑N ^ (1 / 2)) atTop atTop A:Set ℕhAinf:A.InfinitehAsid:IsSidon Ah:liminf (fun N => ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2)) atTop ≠ 0c:ℝhc_pos:c > 0hc:∀ᶠ (N : ℕ) in atTop, c ≤ ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2)⊢ Tendsto (fun N => log ↑N ^ (1 / 2)) atTop atTop simpa using (tendsto_rpow_atTop (A:Set ℕhAinf:A.InfinitehAsid:IsSidon Ah:liminf (fun N => ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2)) atTop ≠ 0c:ℝhc_pos:c > 0hc:∀ᶠ (N : ℕ) in atTop, c ≤ ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2)⊢ 0 < 1 / 2 All goals completed! 🐙 : 0 < 1 / (2 : ℝ))).comp (Real.tendsto_log_atTop.comp tendsto_natCast_atTop_atTop) end Erdos158