FormalConjectures/ErdosProblems/1051.lean

GitHub source file

4 declarations, 2 contain sorry, 0 declared as axioms

1. def Erdos1051.GrowthCondition A sequence of integers a satisfies the growth condition if $\liminf a_n^{\frac{1}{2^n}} > 1$ line 46 source

   Source documentation

   A sequence of integers a satisfies the growth condition if $\liminf a_n^{\frac{1}{2^n}} > 1$.

   The liminf is taken in EReal so that the case $\liminf a_n^{1/2^n} = \infty$ is included; the real-valued liminf of a sequence that is unbounded above defaults to $0$ instead.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Nat, Int

   Proof uses: GT.gt, EReal, Filter.liminf, HPow.hPow, Real, HDiv.hDiv, OfNat.ofNat, Filter.atTop

   25 instances, coercions and auxiliary constants left out.

   def GrowthCondition (a : ℕ → ℤ) : Prop :=
   …

2. def Erdos1051.ErdosSeries The series $\sum_{n=0}^\infty \frac{1}{a_n \cdot a_{n+1}}$ line 52 source

   Source documentation

   The series $\sum_{n=0}^\infty \frac{1}{a_n \cdot a_{n+1}}$.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Nat, Int, Real

   Proof uses: tsum, HDiv.hDiv, OfNat.ofNat, HMul.hMul, HAdd.hAdd, SummationFilter.unconditional

   16 instances, coercions and auxiliary constants left out.

   noncomputable def ErdosSeries (a : ℕ → ℤ) : ℝ :=
   …

3. theorem Erdos1051.erdos_1051 Documented declaration: erdos_1051 sorry line 72 source

   Source documentation

   Is it true that if $a_0 < a_1 < a_2 < \cdots$ is a strictly increasing sequence of integers with $\liminf a_n^{1/2^n} > 1$, then the series $\sum_{n=0}^\infty \frac{1}{a_n \cdot a_{n+1}}$ is irrational?

   This was solved in the affirmative by Aletheia [Fe26]. This was extended by Barreto, Kang, Kim, Kovač, and Zhang [BKKKZ26], who essentially give a complete answer: if $\phi=\frac{1+\sqrt{5}}{2}$ is the golden ratio and $1\leq a_1 < a_2 < \cdots$ is a monotonically increasing sequence of integers such that $\limsup a_n^{1/\phi^{n}}=\infty$ then $\sum_{n=1}^\infty \frac{1}{a_na_{n+1}}$ is irrational. Conversely, for any $1 < C < \infty$ there exists a sequence of integers $1\leq a_1<\cdots$ such that $\lim a_n^{1/\phi^{n}}=C$ where this infinite sum is a rational number.

   (Further, more general, results are available in [BKKKZ26].)

   This was formalized in Lean by Baretto.

   depends on sorry what this means

   Statement uses: Iff, True, Nat, Int, StrictMono, Erdos1051.GrowthCondition, Irrational, Erdos1051.ErdosSeries

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat

   15 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem erdos_1051 :
       answer(True) ↔ ∀ (a : ℕ → ℤ), StrictMono a → GrowthCondition a →
         Irrational (ErdosSeries a) := by
   …

   Mentions: Erdos1051.GrowthCondition, Erdos1051.ErdosSeries

4. theorem Erdos1051.erdos_1051.variants.rapid_growth Erdős [Er88c] notes that if the sequence grows rapidly to infinity (specifically, if $a_{n+1} \geq C \cdot a_n^2$ for some constant $C > 0$), then the series is irrational sorry line 82 source

   Source documentation

   Erdős [Er88c] notes that if the sequence grows rapidly to infinity (specifically, if $a_{n+1} \geq C \cdot a_n^2$ for some constant $C > 0$), then the series is irrational.

   depends on sorry what this means

   Statement uses: Nat, Int, StrictMono, Exists, Real, And, GT.gt, OfNat.ofNat, GE.ge, HAdd.hAdd, HMul.hMul, HPow.hPow, Irrational, Erdos1051.ErdosSeries

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   44 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem erdos_1051.variants.rapid_growth (a : ℕ → ℤ) (h_mono : StrictMono a)
       (h_rapid : ∃ C > 0, ∀ n, (a (n + 1) : ℝ) ≥ C * (a n : ℝ) ^ 2) :
       Irrational (ErdosSeries a) := by
   …

   Mentions: Erdos1051.ErdosSeries