normalized_le_one
plain-language theorem explainer
The theorem shows that for a positive real sequence a the normalized version ã(n) equals a(n) divided by the running maximum up to n and satisfies ã(n) ≤ 1. Navier-Stokes analysts cite the bound when rescaling vorticity fields in hypothetical blowup sequences to obtain scale-invariant controls. The proof is a direct term-mode reduction that unfolds the quotient and invokes the division inequality together with the running-max comparison and positivity lemmas.
Claim. Let $a : ℕ → ℝ$ with $a(n) > 0$. Define the normalized sequence by $ã(n) := a(n) / sup_{k ≤ n} a(k)$. Then $ã(n) ≤ 1$.
background
The module implements running-max normalization for the Navier-Stokes regularity argument (NS Paper §3 Step 1). The running maximum of a sequence a up to index n is the supremum of a(k) for k ≤ n. The normalized sequence is the pointwise quotient a(n) divided by this running maximum, which by construction yields a scale-invariant field whose supremum norm is at most one.
proof idea
The term proof unfolds the definition of normalized and applies div_le_one. The positivity hypothesis on a(n) is fed to runningMax_pos to guarantee a positive denominator, after which runningMax_ge supplies the numerator-denominator comparison that closes the inequality.
why it matters
The result directly supplies the unit bound used by the downstream theorem normalized_vorticity_bounded, which asserts that the rescaled vorticity satisfies ||ω̃_n||_∞ ≤ 1. It completes the first analytic step of the NS paper §3 construction that extracts ancient solutions from a blowing-up sequence. The bound is a prerequisite for the compactness and monotonicity arguments that follow in the regularity theory.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.