Erdős problem 315
Let and , so that and for , where Let be any other sequence with . Is it true that
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/315.leanTrue ↔ ∀ (a : ℕ → ℕ), (∀ (i : ℕ), 0 < a i) → StrictMono a → (∃ i, a i ≠ Erdos315.u i + 1) → ∑' (i : ℕ), 1 / ↑(a i) = 1 → Filter.liminf (fun i => ↑(a i) ^ (1 / 2) ^ (i + 1)) Filter.atTop < Erdos315.c₀Proof manifests naming this Problem
- Jayyhk Erdős Lean
jayyhk:erdos:315 - PLBY Lean proofs
ErdosProblems.Erdos315
Reported activity
Work these sources record against this Problem. Source-reported attribution, not reviewed here.
Formalization
- Machine