runningMax_mono
plain-language theorem explainer
Monotonicity of the running maximum holds for any real sequence indexed by naturals. Navier-Stokes analysts invoke it when normalizing vorticity in blow-up analysis to extract scale-invariant bounds. The term proof reduces the claim to Finset supremum comparison via range inclusion.
Claim. For any sequence $a : ℕ → ℝ$, the map $n ↦ sup {a(k) | k ≤ n}$ is monotone non-decreasing.
background
The RunningMaxNormalization module formalizes the running-max construction for Navier-Stokes regularity (NS Paper §3, Step 1). Given a sequence of sup-norms $M_n → ∞$, it builds the running maximum $M̃(t) = sup_{s ≤ t} M(s)$ to produce normalized fields with $L^∞$ norm at most 1, as described in the module documentation. This step uses only monotone sequence theory and sup properties, standard in Caffarelli-Kohn-Nirenberg and Escauriaza-Seregin-Šverák arguments.
proof idea
The term-mode proof introduces indices $m ≤ n$, unfolds the runningMax definition, applies Finset.sup'_le, and for each $k$ in the smaller range shows membership in the larger sup by invoking Finset.le_sup' after range_mono with omega.
why it matters
It supplies the monotone component of the RunningMaxCert record used by runningMaxCert and runningMax_tendsto_atTop. This completes the initial normalization step in the Navier-Stokes blow-up analysis, supporting extraction of ancient elements and aligning with phi-forcing and the eight-tick octave in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.