rescaleLength
The rescaling length λ_n is defined as the reciprocal square root of the running maximum of a sequence a up to n. Analysts studying potential singularities in the Navier-Stokes equations cite this when rescaling a blowing-up sequence to obtain a bounded ancient solution. The definition is a direct algebraic expression using the running maximum.
claim$λ_n = 1 / √(M̃(n))$ where $M̃(n) = max_{k ≤ n} a(k)$ for a sequence $a : ℕ → ℝ$.
background
The module formalizes running-max normalization for the Navier-Stokes regularity proof to extract ancient elements from a blowing-up sequence. The running maximum M̃(n) of a sequence a is defined as the supremum over the first n+1 terms via Finset.sup' on the range up to n. This setup produces scale-invariant fields with normalized L^∞ norm bounded by 1, following the standard approach in Caffarelli-Kohn-Nirenberg and Escauriaza-Seregin-Šverák.
proof idea
The definition directly computes the reciprocal square root of the running maximum applied to the sequence a at n. It relies on the prior definition of runningMax without additional lemmas or tactics.
why it matters in Recognition Science
This supplies the spatial rescaling factor in the normalization procedure for the Navier-Stokes regularity argument. It is used directly by the positivity result rescaleLength_pos and the limit result rescaleLength_tendsto_zero. The construction follows the standard real-analysis step in the NS paper §3 for handling hypothetical blowups.
scope and limits
- Does not assert positivity of the factor.
- Does not address the limit behavior as the maximum diverges.
- Does not embed the Navier-Stokes equations.
- Does not cover sequences with zero values.
formal statement (Lean)
91noncomputable def rescaleLength (a : ℕ → ℝ) (n : ℕ) : ℝ :=
proof body
Definition body.
92 1 / Real.sqrt (runningMax a n)
93
94/-- The rescaling factor is positive. -/