normalized_le_one
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove convergence or monotonicity of the normalized sequence.
- Does not apply when any term of a is non-positive.
- Does not treat the continuous-time version of the running maximum.
- Does not address higher-dimensional or vector-valued analogues.
Lean usage
exact normalized_le_one M n (hpos n)formal statement (Lean)
74theorem normalized_le_one (a : ℕ → ℝ) (n : ℕ) (h : 0 < a n) :
75 normalized a n ≤ 1 := by
proof body
Term-mode proof.
76 unfold normalized
77 exact (div_le_one (runningMax_pos a n h)).mpr (runningMax_ge a n)
78
79/-- The normalized sequence achieves 1 at the running-max index. -/