runningMax
The running maximum of a real sequence a at each n is the supremum of a(k) for all k from 0 to n. Navier-Stokes regularity analysts cite this operator when normalizing hypothetical blow-up sequences to extract ancient solutions. The definition is realized directly as the finite-set supremum of the initial segment of the naturals.
claimFor a sequence $a : ℕ → ℝ$, define the running maximum by $M̃(n) := sup_{k ≤ n} a(k)$.
background
This module formalizes the running-max normalization used in the Navier-Stokes regularity proof to extract ancient elements from a blowing-up sequence. Given times tₙ → T* and sup-norms Mₙ = ‖ω(·,tₙ)‖{L^∞} with Mₙ → ∞, the construction sets M̃(t) = sup{s ≤ t} M(s) and produces normalized fields ũ(x,t) = u(x,t) / M̃(tₙ) on rescaled coordinates so that ‖ω̃(·,tₙ)‖_{L^∞} ≤ 1. The module relies only on monotone sequence theory and supremum properties, as in Caffarelli-Kohn-Nirenberg and Escauriaza-Seregin-Šverák.
proof idea
One-line wrapper that applies Finset.sup' to the range (n+1) together with the nonempty-range proof.
why it matters in Recognition Science
This definition supplies the core operator used by normalized, rescaleLength, and RunningMaxCert in the same module. It implements the first step of the Navier-Stokes regularity argument in §3 of the paper, enabling bounded rescaled vorticity. The construction preserves scale-invariant properties that align with the Recognition framework's phi-ladder and eight-tick octave.
scope and limits
- Does not extend the construction to continuous-time functions.
- Does not assume positivity or monotonicity of the input sequence.
- Does not compute the limit of the running maximum.
- Does not address convergence rates or asymptotic behavior.
Lean usage
noncomputable def normalized (a : ℕ → ℝ) (n : ℕ) : ℝ := a n / runningMax a nformal statement (Lean)
33noncomputable def runningMax (a : ℕ → ℝ) : ℕ → ℝ :=
proof body
Definition body.
34 fun n => Finset.sup' (Finset.range (n + 1))
35 (Finset.nonempty_range_add_one) a
36
37/-- The running maximum is always ≥ the current value. -/