FormalConjectures.ErdosProblems.«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 Realnamespace 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 := byA: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₂
    wlog h₁ : a₁ ≤ b₁inrA: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₂
    ·inrA: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₂ have := this hA _ hb₁ _ ha₂ _ ha₁ _ hb₂inrA: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₂⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
      grindAll goals completed! 🐙
    wlog h₂ : a₂ ≤ b₂inrA: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₂
    ·inrA: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₂ have := this hA _ ha₁ _ hb₂ _ hb₁ _ ha₂inrA: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₂⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
      clear ha₁ ha₂ hb₁ hb₂inrA: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₂⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
      grindAll goals completed! 🐙
    have := Set.encard_le_one_iff.1 (hA (a₁ + b₁)) ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ (byA: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}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₂this:(a₁, b₁) = (a₂, b₂)⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂ simp [*]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₂this:(a₁, b₁) = (a₂, b₂)⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂) (byA: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}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₂this:(a₁, b₁) = (a₂, b₂)⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂ simp [*]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₂this:(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₂h₁:a₁ ≤ b₁h₂:a₂ ≤ b₂this:(a₁, b₁) = (a₂, b₂)⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
    grindAll goals completed! 🐙
  mpr hA n := byA:Set ℕhA:IsSidon An:ℕ⊢ {x | x.1 + x.2 = n ∧ x.1 ≤ x.2 ∧ x.1 ∈ A ∧ x.2 ∈ A}.encard ≤ ↑1
    refine Set.encard_le_one_iff.2 fun x y ⟨h, p, q⟩ ⟨r, s, t⟩ => ?_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
    have := hA x.1 q.1 y.1 t.1 x.2 q.2 y.2 t.2 (h.trans r.symm)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⊢ x = y
    grindAll 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 erdos_158 : answer(sorry) ↔ ∀ A : Set ℕ, A.Infinite → B2 2 A →
    liminf (fun N : ℕ => (A ∩ .Iio N).ncard * (N : ℝ) ^ (- 1 / 2 : ℝ)) atTop = 0 := by⊢ True ↔ ∀ (A : Set ℕ), A.Infinite → B2 2 A → liminf (fun N ↦ ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2)) atTop = 0
  sorryAll 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 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 < ⊤ := byA:Set ℕhAinf:A.InfinitehAsid:IsSidon A⊢ liminf (fun N ↦ ENNReal.ofReal (↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2) * log ↑N ^ (1 / 2))) atTop < ⊤
  sorryAll 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 := byA:Set ℕhAinf:A.InfinitehAsid:IsSidon A⊢ liminf (fun N ↦ ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2)) atTop = 0
  have := erdos_158.variants.isSidon' hAinf hAsidA:Set ℕhAinf:A.InfinitehAsid:IsSidon Athis:liminf (fun N ↦ ENNReal.ofReal (↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2) * log ↑N ^ (1 / 2))) atTop < ⊤⊢ liminf (fun N ↦ ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2)) atTop = 0
  contrapose! this with hA: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
  rw [Tendsto.liminf_eqA:Set ℕhAinf:A.InfinitehAsid:IsSidon Ah:liminf (fun N ↦ ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2)) atTop ≠ 0⊢ ⊤ ≤ ?m.52A: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 ?m.52)A:Set ℕhAinf:A.InfinitehAsid:IsSidon Ah:liminf (fun N ↦ ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2)) atTop ≠ 0⊢ ENNRealA: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 ↦ ENNReal.ofReal (↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2) * log ↑N ^ (1 / 2))) atTop (nhds ⊤)
  refine ENNReal.tendsto_ofReal_atTop.comp ?_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 : ℝ) := byA: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)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 ↦ ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2) * log ↑N ^ (1 / 2)) atTop atTop
    suffices
      ∃ a ∈ {a | ∃ c : ℕ, ∀ b ≥ c, a ≤ ↑(A ∩ .Iio b).ncard * (b : ℝ) ^ (-1 / 2 : ℝ)}, 0 < a byA: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⊢ ∃ c > 0, ∀ᶠ (N : ℕ) in atTop, c ≤ ↑(A ∩ Set.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⊢ ∃ a ∈ {a | ∃ c, ∀ b ≥ c, a ≤ ↑(A ∩ Set.Iio b).ncard * ↑b ^ (-1 / 2)}, 0 < aA: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 ↦ ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2) * log ↑N ^ (1 / 2)) atTop atTop aesopA:Set ℕhAinf:A.InfinitehAsid:IsSidon Ah:liminf (fun N ↦ ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2)) atTop ≠ 0⊢ ∃ a ∈ {a | ∃ c, ∀ b ≥ c, a ≤ ↑(A ∩ Set.Iio b).ncard * ↑b ^ (-1 / 2)}, 0 < aA: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 ↦ ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2) * log ↑N ^ (1 / 2)) atTop atTopA:Set ℕhAinf:A.InfinitehAsid:IsSidon Ah:liminf (fun N ↦ ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2)) atTop ≠ 0⊢ ∃ a ∈ {a | ∃ c, ∀ b ≥ c, a ≤ ↑(A ∩ Set.Iio b).ncard * ↑b ^ (-1 / 2)}, 0 < aA: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 ↦ ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2) * log ↑N ^ (1 / 2)) atTop atTop
    by_contra! haA: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⊢ FalseA: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 ↦ ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2) * log ↑N ^ (1 / 2)) atTop atTop
    simp only [liminf_eq, eventually_atTop] at hA: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 ≤ b → a ≤ ↑(A ∩ Set.Iio b).ncard * ↑b ^ (-1 / 2)} ≠ 0⊢ FalseA: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 ↦ ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2) * log ↑N ^ (1 / 2)) atTop atTop
    exact h <| le_antisymm (csSup_le ⟨0, 0, fun n hn => byA: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 ≤ b → a ≤ ↑(A ∩ Set.Iio b).ncard * ↑b ^ (-1 / 2)} ≠ 0n:ℕhn:0 ≤ n⊢ 0 ≤ ↑(A ∩ Set.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 ≠ 0c:ℝhc_pos:c > 0hc:∀ᶠ (N : ℕ) in atTop, c ≤ ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2)⊢ Tendsto (fun N ↦ ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2) * log ↑N ^ (1 / 2)) atTop atTop positivityAll 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 ↦ ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2) * log ↑N ^ (1 / 2)) atTop atTop⟩ ha) <|
      (le_csSup ⟨0, ha⟩ ⟨0, fun n hn => byA: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 ≤ b → a ≤ ↑(A ∩ Set.Iio b).ncard * ↑b ^ (-1 / 2)} ≠ 0n:ℕhn:0 ≤ n⊢ 0 ≤ ↑(A ∩ Set.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 ≠ 0c:ℝhc_pos:c > 0hc:∀ᶠ (N : ℕ) in atTop, c ≤ ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2)⊢ Tendsto (fun N ↦ ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2) * log ↑N ^ (1 / 2)) atTop atTop positivityAll 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 ↦ ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2) * 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 ↦ ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2) * log ↑N ^ (1 / 2)) atTop atTop
  refine tendsto_atTop_mono' atTop (f₁ := fun N : ℕ => c * log N ^ (1 / 2 : ℝ)) ?_ ?_refine_1A: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)refine_2A: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
  ·refine_1A: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 hnA: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 [hnA: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)⊢ ↑(A ∩ Set.Iio n).ncard * ↑n ^ (-1 / 2) * log ↑n ^ (1 / 2) ≤ ↑(A ∩ Set.Iio n).ncard * ↑n ^ (-1 / 2) * log ↑n ^ (1 / 2)]All goals completed! 🐙
  ·refine_2A: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 refine .const_mul_atTop hc_pos ?_refine_2A: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 [Function.comp_def] using (tendsto_rpow_atTop (byA: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 linarithAll goals completed! 🐙 : 0 < 1 / (2 : ℝ))).comp
      (Real.tendsto_log_atTop.comp tendsto_natCast_atTop_atTop)

end Erdos158