runningMax_ge
plain-language theorem explainer
The inequality asserts that for any real sequence a indexed by naturals, the value at n is at most the running maximum up to n. Analysts working on blowup criteria in fluid equations cite this basic comparison when constructing normalized sequences from diverging sup-norms. The proof is a one-line wrapper that unfolds the definition of runningMax as a Finset supremum and applies the standard le_sup' property.
Claim. For any sequence $a : ℕ → ℝ$ and natural number $n$, $a(n) ≤ sup_{k ≤ n} a(k)$.
background
The running maximum is defined as the supremum of the initial segment: runningMax a n = Finset.sup' (Finset.range (n+1)) (Finset.nonempty_range_add_one) a. The module formalizes running-max normalization for the Navier-Stokes regularity proof to extract ancient elements from a blowing-up sequence, constructing M̃(t) = sup_{s ≤ t} M(s) where M(t) = ‖ω(·,t)‖_{L^∞} and normalized fields ũ(x,t) = u(x,t) / M̃(tₙ) on rescaled coordinates. This is standard (Caffarelli-Kohn-Nirenberg, Escauriaza-Seregin-Šverák) and requires only monotone sequence theory plus sup properties. The upstream result is the definition of runningMax itself.
proof idea
One-line wrapper that unfolds the definition of runningMax and applies Finset.le_sup' followed by simp.
why it matters
This comparison is invoked by normalized_le_one to bound the rescaled sequence by 1 and by runningMax_pos to establish positivity. It supports the construction in the Navier-Stokes regularity argument that normalizes blowing-up sequences to produce bounded ancient solutions, as described in the module documentation for NS Paper §3 Step 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.