runningMax_tendsto_atTop
plain-language theorem explainer
If a real sequence diverges to infinity then its running maximum diverges to infinity as well. Analysts working on Navier-Stokes regularity invoke this to normalize sequences whose L^infty norms blow up. The argument rewrites the tendsto_atTop definition twice, extracts a witness index from the hypothesis, and chains the lower-bound and monotonicity facts for the running maximum via order transitivity.
Claim. Let $(a_n)_{n=0}^∞$ be a sequence of real numbers with $a_n → +∞$ as $n → ∞$. Let $M_n = max_{k ≤ n} a_k$. Then $M_n → +∞$ as $n → ∞$.
background
The running maximum of a sequence $a : ℕ → ℝ$ is the function $M(n) = sup {a(k) | k ≤ n}$, realized as the supremum over the finite initial segment via Finset.sup'. This module supplies the first step of the running-max normalization used in the Navier-Stokes regularity argument (NS Paper §3), where one rescales vorticity fields by a monotone majorant that diverges whenever the original sup-norms diverge. Upstream results include the lower-bound property that the running maximum is always at least the current term and the monotonicity property that the running maximum is non-decreasing; order transitivity is the only external arithmetic fact required.
proof idea
The proof is a term-mode construction after two rewrites of Filter.tendsto_atTop_atTop. Fix an arbitrary real bound b. The hypothesis supplies N such that a exceeds b beyond N. The same N works for the running maximum because runningMax a N ≥ a N and the running maximum is monotone, so the value at all larger indices stays above b. The exact term applies le_trans twice to combine the lower bound, monotonicity, and the witness from the hypothesis.
why it matters
This lemma guarantees divergence of the running maximum and is invoked directly by rescaleLength_tendsto_zero to show that the rescaling factor vanishes. It therefore closes the first step of the normalization construction in the Navier-Stokes regularity analysis, producing scale-invariant normalized fields without extra hypotheses. The result sits inside the pure real-analysis layer that precedes any appeal to the Recognition Science forcing chain or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.