rescaleLength
plain-language theorem explainer
RescaleLength supplies the factor λ_n = 1 over square root of the running maximum of sequence a at step n. Navier-Stokes regularity analysts cite it when normalizing a blowing-up vorticity sequence to extract an ancient limit with unit sup-norm. The definition is a direct one-line algebraic expression built on the running-max construction.
Claim. Define the rescaling factor by $λ_n := 1 / √M(n)$, where $M(n)$ is the running maximum of the input sequence $a$ up to index $n$. This factor is used to rescale space by $x ↦ x/λ_n$ and time by $t ↦ t/λ_n²$.
background
RunningMax constructs the monotone envelope M̃(n) = max_{k≤n} a(k) via finite suprema over initial segments. The module implements the first step of the Navier-Stokes regularity argument: given a hypothetical blow-up sequence with M_n → ∞, the running maximum produces a normalized field whose L^∞ norm is bounded by 1. This construction is the standard real-analysis device appearing in Caffarelli-Kohn-Nirenberg and Escauriaza-Seregin-Šverák.
proof idea
One-line definition that applies the runningMax construction and takes the reciprocal square root.
why it matters
The definition supplies the explicit length scale for the normalization step in the NS regularity argument. It is the direct input to the downstream theorems rescaleLength_pos and rescaleLength_tendsto_zero that establish positivity and the limit to zero. It implements the scale-invariant extraction described in the module as NS Paper §3 Step 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.