rescaleLength_pos
plain-language theorem explainer
The positivity of the rescaling length factor follows from the positivity of the running maximum via square-root and division rules. Analysts constructing normalized ancient solutions from hypothetical Navier-Stokes blow-up sequences cite this lemma to guarantee a well-defined positive scale factor. The proof is a one-line term-mode reduction that unfolds the definition and applies standard positivity facts for division and square roots.
Claim. Let $a : ℕ → ℝ$, $n ∈ ℕ$, and suppose $a_n > 0$. Then $0 < λ_n$ where $λ_n = 1 / √(sup_{k ≤ n} a_k)$.
background
The module implements the running-max normalization step in the Navier-Stokes regularity argument. The running maximum of sequence a up to index n is the least upper bound of the values a_0 through a_n. The rescaling length is defined as the reciprocal of the square root of this running maximum and is used to rescale space by λ_n and time by λ_n² so that the normalized vorticity satisfies a uniform L^∞ bound of 1.
proof idea
The term proof unfolds the definition of rescaleLength to expose the division 1 / √(runningMax a n), applies the lemma div_pos with the constant 1 shown positive, and closes by invoking Real.sqrt_pos.mpr on the runningMax_pos theorem applied to the hypothesis 0 < a n.
why it matters
The lemma supplies the positivity needed for the rescaling construction in the Navier-Stokes blow-up analysis. It directly supports the extraction of ancient elements with bounded normalized vorticity as described in the module documentation. No downstream uses are recorded yet; the result closes a basic positivity obligation in the normalization pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.