runningMax_pos
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.
claimLet $(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 in Recognition Science
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.
scope and limits
- Does not apply when every term of the sequence is non-positive.
- Does not control the growth rate of the running maximum.
- Does not extend to continuous-time suprema without an auxiliary discretization.
- Does not treat complex-valued or vector-valued sequences.
formal statement (Lean)
62theorem runningMax_pos (a : ℕ → ℝ) (n : ℕ) (h : 0 < a n) :
63 0 < runningMax a n :=
proof body
Term-mode proof.
64 lt_of_lt_of_le h (runningMax_ge a n)
65
66/-! ## Normalization -/
67
68/-- The normalized sequence: ã(n) = a(n) / runningMax(a)(n).
69 By construction, |ã(n)| ≤ 1 for all n. -/