runningMax_pos
plain-language theorem explainer
The running maximum of a real sequence is strictly positive at any index where the sequence value itself is positive. Analysts working on blow-up criteria for the Navier-Stokes equations cite this to keep normalization factors well-defined and positive. The proof is a one-line term that transfers positivity via the domination property of the running maximum.
Claim. Let $(a_k)_{k∈ℕ}$ be a sequence of real numbers. If $a_n>0$ for a fixed index $n$, then the running maximum $M_n=sup_{k≤n}a_k$ satisfies $M_n>0$.
background
In the Navier-Stokes regularity analysis a running maximum is constructed from a sequence of vorticity sup-norms $M(t)=‖ω(·,t)‖{L^∞}$ by taking the monotone envelope $M̃(t)=sup{s≤t}M(s)$. This supplies the denominator for normalized fields ũ(x,t)=u(x,t)/M̃(t_n) whose $L^∞$ norm is at most one by construction. The module implements the first step of the standard blow-up extraction procedure (Caffarelli-Kohn-Nirenberg, Escauriaza-Seregin-Šverák) using only finite-supremum properties of real sequences.
proof idea
The argument is a one-line term proof that applies the companion inequality runningMax a n ≥ a n to the hypothesis 0 < a n and invokes transitivity of the strict order on the reals.
why it matters
The result supplies the positivity needed for the normalized-sequence bounds and the positive rescaling length that follow in the same module. It closes the basic well-definedness check in the running-max normalization step of the NS paper §3, enabling the subsequent compactness arguments that extract ancient solutions. No scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.