Tao Theorem 1.3: almost all Collatz orbits attain almost bounded values
Opencollatz_almost_bounded_logarithmiccollatznumber-theory
For every real-valued function f tending to infinity on positive integer inputs, the positive inputs n whose Collatz orbit contains a value strictly below f(n) form a set of logarithmic density one. The real-cutoff reciprocal mass is normalized by log x; the full orbit includes its starting value. This is not natural density, a fixed absolute bound, or convergence of every orbit to one.
Preamble
import Mathlib import Definitions.Def_collatzStepMap import Definitions.Def_weightedLogMassReal open Filter open scoped Topology
Formal statement
theorem collatz_almost_bounded_logarithmic (f : ℕ → ℝ) (hf : ∀ M : ℝ, ∃ N : ℕ, ∀ n : ℕ, N ≤ n → 0 < n → M < f n) : Tendsto (fun x : ℝ => weightedLogMassReal (fun n => 0 < n) (fun n => ∃ k : ℕ, ((collatzStep^[k] n : ℕ) : ℝ) < f n) (fun n => 1 / (n : ℝ)) x) atTop (𝓝 (1 : ℝ)) := by sorry
Source
Terence Tao, Almost all orbits of the Collatz map attain almost bounded values, Forum of Mathematics, Pi 10 (2022), e12; arXiv:1909.03562v7, Theorem 1.3. https://arxiv.org/html/1909.03562v7
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.