normalized_le_one
plain-language theorem explainer
The theorem shows that the normalized sequence ã(n) = a(n) / runningMax(a)(n) is at most 1 whenever a(n) > 0. Analysts working on Navier-Stokes regularity would cite this to bound rescaled vorticity after running-max normalization. The proof is a one-line term reduction that unfolds the definition and applies the division lemma to the running-maximum inequalities.
Claim. Let $(a_n)_{n∈ℕ}$ be a sequence of real numbers and $n∈ℕ$ with $a_n>0$. Then $a_n / sup_{k≤n} a_k ≤ 1$.
background
The module formalizes the running-max normalization used in the Navier-Stokes regularity proof to extract ancient elements from a blowing-up sequence. Given times $t_n→T^*$ and sup-norms $M_n=‖ω(·,t_n)‖{L^∞}$ with $M_n→∞$, the running maximum is $M̃(t)=sup{s≤t}M(s)$ and the normalized sequence is ã(n)=a(n)/runningMax(a)(n). The module documentation states that this yields scale-invariant properties with ‖ω̃(·,t_n)‖_{L^∞}≤1 by construction and requires only monotone sequence theory plus sup properties.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the definition of normalized, then applies div_le_one to the positivity of the running maximum (from runningMax_pos) and the fact that the running maximum is at least the current term (from runningMax_ge).
why it matters
This supplies the bound used by normalized_vorticity_bounded, which states that the normalized vorticity satisfies ‖ω̃_n‖≤1 for all n. It fills the running-max normalization step in NS Paper §3, Step 1, ensuring the rescaled sequence remains bounded after division by the running maximum. The construction is standard in the Caffarelli-Kohn-Nirenberg approach to regularity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.