runningMax
plain-language theorem explainer
The running maximum of a sequence a : ℕ → ℝ is the pointwise supremum of its initial segments. Navier-Stokes analysts working on blowup criteria cite this to normalize diverging L^∞ vorticity sequences before rescaling. The definition is realized by a direct call to the nonempty finite supremum operator on the range up to n+1.
Claim. Let $a : ℕ → ℝ$. The running maximum is the function $M(n) := sup_{k ≤ n} a(k)$.
background
The module implements the first step of the running-max normalization procedure described in the NS paper §3. Given a sequence of times with diverging sup-norms M_n → ∞, one forms the running maximum M̃(n) = sup_{k ≤ n} M(k) so that the rescaled fields satisfy ||ω̃(·, t_n)||_∞ ≤ 1. This construction relies only on the monotone sequence theory and finite-sup properties already available in Mathlib. The local setting is pure real analysis inside the larger Recognition Science formalization of Navier-Stokes regularity.
proof idea
One-line definition that applies Finset.sup' to Finset.range (n+1) using the supplied nonempty proof Finset.nonempty_range_add_one.
why it matters
This definition is the root of the normalization pipeline. It is used by normalized, rescaleLength, RunningMaxCert, and the monotonicity and positivity lemmas that follow. The construction directly supports the extraction of ancient elements from hypothetical blowup sequences in the NS regularity argument. It fills the initial concrete step of the running-max procedure before any Recognition Science constants or J-cost arguments enter.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.