Problem

The intuition is as follows: for any $y$ in the range of $f$, there exists a strictly increasing sequence of points $\{x_1,x_2,\dots \}$ such that $y=\underset{i\to \mathrm{\infty }}{lim}f(x_i)$.

Proof

A point $y\in \mathbb{R}$ is called a cluster point of $f$ as $x\to +\mathrm{\infty }$ if there exists a sequence $\{x_n{\}}_{n\in \mathbb{N}}$ such that $x_n\to +\mathrm{\infty }$ as $n\to \mathrm{\infty }$ and $f(x_n)\to y$ as $n\to \mathrm{\infty }$.

Define the sequence $\{x_n\}$ as $x_n=x_0+nT$ for all $n\in \mathbb{N}$.
Since $T>0$, for any $B\in \mathbb{R}$, there exists an integer $N=\lceil \frac{B-x_0}{T}\rceil$ such that for all $n\ge N$:

Consequently, $\underset{n\to \mathrm{\infty }}{lim}{x}_n=+\mathrm{\infty }$.

Using the periodicity of $f$, we show by induction that $f(x_n)=y$ for any $n\in \mathbb{N}$:

• $f(x_0)=y$.
• If $f(x_0+nT)=f(x_0)$, then $f(x_0+(n+1)T)=f((x_0+nT)+T)=f(x_0)=y$.

Thus,

Therefore, $y\in \text{Lim}(f,+\mathrm{\infty }).$

Lean

The formal proof of lemma verified in Lean:

import Mathlib.Topology.Basic
import Mathlib
open Set Filter Topology

theorem periodic_cluster_pt
  {f : ℝ → ℝ} {T : ℝ}
  (hT : 0 < T)
  (h_per : ∀ x, f (x + T) = f x) :

  ∀ y ∈ range f, MapClusterPt y atTop f := by
  intro y hy
  rcases hy with ⟨x₀, rfl⟩

  -- Define sequence xₙ = x₀ + nT
  let x : ℕ → ℝ := fun n => x₀ + n * T

  have hx_tendsto : Tendsto x atTop atTop := by
    rw [tendsto_atTop_atTop]
    intro B
    have hmul : Tendsto (fun n : ℕ => (n : ℝ) * T) atTop atTop :=
      tendsto_natCast_atTop_atTop.atTop_mul_const' hT
    rcases (tendsto_atTop_atTop.mp hmul) (B - x₀ + 1) with ⟨N, hN⟩
    use N
    intro n hn
    have h : (n : ℝ) * T ≥ B - x₀ + 1 := hN n hn
    unfold x
    linarith

  -- f(xₙ) = f(x₀)
  have h_const : ∀ n, f (x n) = f x₀ := by
    intro n
    induction n with
    | zero =>
        simp [x]
    | succ n ih =>
        have : x₀ + (n + 1) * T = (x₀ + n * T) + T := by ring
        simp [x, this, h_per, ih]

  -- Therefore, f ∘ x → y
  have h_fx_tendsto : Tendsto (fun n => f (x n)) atTop (𝓝 (f x₀)) := by
    have : (fun n => f (x n)) = fun _ => f x₀ := by
      funext n
      exact h_const n
    simp [this]

  -- Show that (𝓝 (f x₀) ⊓ map f atTop).NeBot
  have h_both : Tendsto (fun n => f (x n)) (atTop ⊓ atTop) (𝓝 (f x₀) ⊓ map (f ∘ x) atTop) :=
    h_fx_tendsto.inf tendsto_map
  have h_neBot : (𝓝 (f x₀) ⊓ map (f ∘ x) atTop).NeBot := by
    rw [inf_idem] at h_both
    exact h_both.neBot

  -- Prove MapClusterPt
  rw [MapClusterPt, ClusterPt]
  apply h_neBot.mono
  apply inf_le_inf_left
  rw [← map_map]
  apply map_mono
  exact hx_tendsto