normalized_vorticity_bounded
plain-language theorem explainer
The theorem asserts that the normalized sequence obtained by dividing each term of a positive sequence M by its running maximum is bounded above by 1 at every index. Navier-Stokes regularity researchers cite it when rescaling hypothetical blow-up sequences of vorticity to produce scale-invariant ancient solutions. The proof is a direct one-line application of the general normalized_le_one lemma instantiated at the given index.
Claim. Let $M : ℕ → ℝ$ be a sequence satisfying $M(n) > 0$ for every $n ∈ ℕ$. Define the normalized sequence by $˜M(n) = M(n) / sup_{k ≤ n} M(k)$. Then $˜M(n) ≤ 1$ holds for all $n$.
background
The running-max normalization divides each term of a sequence by the supremum of all preceding terms (including itself) to produce a scale-invariant version bounded by 1. The module implements this construction to extract bounded ancient elements from a hypothetical blow-up sequence of vorticity sup-norms in the Navier-Stokes regularity argument. The supporting lemma normalized_le_one states that for any positive sequence a the normalized version satisfies normalized a n ≤ 1, proved by unfolding the definition and applying the running-max properties.
proof idea
The proof is a one-line wrapper that applies the lemma normalized_le_one to the sequence M at index n, supplying the positivity hypothesis hpos n.
why it matters
This supplies the uniform bound required by the downstream theorem normalized_bounded, which in turn supports the extraction of ancient solutions in the Navier-Stokes blow-up analysis (NS Paper §3, Step 1). It completes the basic boundedness step of the running-max construction before rescaling arguments begin.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.