normalized_le_one
plain-language theorem explainer
The running-max normalized sequence satisfies ã(n) ≤ 1 whenever a(n) > 0. Analysts formalizing Navier-Stokes regularity would cite the bound to control rescaled L^∞ norms after blow-up extraction. The argument is a one-line term proof that invokes the division inequality on the running-max lower bound together with positivity preservation.
Claim. Let $(a_n)_{n∈ℕ}$ be a sequence of real numbers and $n∈ℕ$ with $a_n>0$. Let $M_n=sup_{k≤n}a_k$. Then $a_n/M_n≤1$.
background
The module implements the first step of the Navier-Stokes regularity argument (NS Paper §3, Step 1). It replaces a hypothetical blow-up sequence of sup-norms $M_n→∞$ by the normalized sequence ã(n) := a(n)/runningMax(a)(n), where runningMax(a)(n) is the supremum of a(k) for k≤n. The normalized definition is given directly as a(n) divided by that running maximum, and the module states that the construction is standard (Caffarelli-Kohn-Nirenberg, Escauriaza-Seregin-Šverák) and uses only monotone sequence theory plus sup properties.
proof idea
The proof unfolds the definition of normalized and applies the division inequality div_le_one to the positivity of the running maximum (runningMax_pos) together with the fact that the current value is at most the running maximum (runningMax_ge). It is a one-line term proof.
why it matters
This bound directly justifies the claim that the normalized vorticity satisfies ‖ω̃_n‖≤1 for all n, which is recorded as normalized_vorticity_bounded. It supplies the concrete first step in the running-max normalization procedure of NS Paper §3, ensuring the rescaled sequence remains bounded. In the Recognition framework the construction supports extraction of ancient solutions from blow-up sequences, a prerequisite for regularity analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.