runningMax_ge
plain-language theorem explainer
Every term of a real sequence on the naturals is bounded above by its running maximum up to that index. Analysts formalizing blow-up criteria for Navier-Stokes cite this to control normalized fields extracted from divergent sequences. The proof is a term-mode wrapper that unfolds the finite-supremum definition and applies the standard le_sup' property.
Claim. Let $a : ℕ → ℝ$ be any sequence and $n ∈ ℕ$. Then $a(n) ≤ sup_{k=0 to n} a(k)$, where the supremum is taken over the initial segment of the sequence.
background
The running maximum is defined by taking the supremum of sequence values over the finite initial segment Finset.range (n+1) via Finset.sup'. The module sets up running-max normalization to extract ancient elements from a hypothetical blow-up sequence in the Navier-Stokes regularity argument (NS Paper §3, Step 1), ensuring the normalized fields satisfy a uniform L^∞ bound of 1. This rests on the elementary properties of finite suprema over monotone index sets.
proof idea
Term-mode proof that unfolds the runningMax definition then applies Finset.le_sup' and simp to verify membership in the range.
why it matters
The result supplies the elementary comparison used by normalized_le_one to bound the normalized sequence by 1 and by runningMax_pos to obtain positivity. It completes the first step of the running-max construction in the Navier-Stokes module, which feeds the scale-invariant extraction of ancient solutions. The surrounding framework uses this to reach the regularity claim via the eight-tick octave and phi-ladder mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.