runningMax
plain-language theorem explainer
The running maximum supplies the monotone envelope M̃(n) = max_{k≤n} a(k) for sequences in blow-up analysis. Navier-Stokes regularity researchers cite it to build normalized fields bounded by 1 and rescaling factors that tend to zero. The definition is a direct encoding of the finite supremum over the initial segment via Finset.sup'.
Claim. For a sequence $a : ℕ → ℝ$, define the running maximum by $M̃(n) := max_{k=0,…,n} a(k)$.
background
The module formalizes running-max normalization for the Navier-Stokes regularity argument (NS Paper §3, Step 1). Given a sequence of times tₙ → T* with sup-norms Mₙ = ‖ω(·,tₙ)‖{L^∞} diverging to infinity, the construction produces a monotone envelope M̃(t) = sup{s≤t} M(s), normalized fields ũ(x,t) = u(x,t)/M̃(tₙ) on rescaled coordinates, and scale-invariant bounds ‖ω̃(·,tₙ)‖_{L^∞} ≤ 1. This rests only on monotone sequence theory and supremum properties, matching the standard approach of Caffarelli-Kohn-Nirenberg and Escauriaza-Seregin-Šverák.
proof idea
One-line definition that applies Finset.sup' to the range (n+1) with the nonempty_range_add_one witness.
why it matters
It is the base definition feeding normalized, rescaleLength, RunningMaxCert, runningMax_ge, runningMax_mono and runningMax_pos inside the same module. The module doc positions it as the first concrete step in the NS regularity proof that extracts ancient elements from a hypothetical blow-up sequence. No direct tie to the T0-T8 forcing chain or RCL appears here; the construction remains standard real analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.