runningMax_ge
The inequality asserts that every term of a real sequence is bounded above by its running maximum up to that index. Analysts formalizing Navier-Stokes regularity would cite it when normalizing vorticity sequences that may diverge. The proof is a one-line term application of the finite-supremum definition together with the standard element-to-sup property.
claimFor any sequence of real numbers $a:ℕ→ℝ$ and any natural number $n$, $a_n≤sup_{0≤k≤n}a_k$.
background
The running maximum of a sequence $a$ is the function that returns the supremum of $a$ over the finite initial segment $0$ to $n$. This construction is introduced in the running-max normalization module to extract scale-invariant fields from hypothetical blow-up sequences in the Navier-Stokes equations, where $M_n=‖ω(·,t_n)‖_{L^∞}$ diverges. The module documentation states that the construction requires only monotone sequence theory and sup properties and is standard in the Caffarelli-Kohn-Nirenberg approach.
proof idea
The term-mode proof unfolds the definition of the running maximum as the supremum over the range up to $n$ and applies the lemma that each element of a finite set is at most the supremum of that set, followed by simplification.
why it matters in Recognition Science
This inequality is invoked directly by normalized_le_one to obtain the bound of 1 on the normalized sequence and by runningMax_pos to obtain positivity. It supplies the elementary comparison needed for the first step of the Navier-Stokes regularity argument in the module, which extracts ancient elements from blowing-up sequences. The result sits inside the pure-analysis layer that supports the scale-invariant properties used later in the Recognition Science chain.
scope and limits
- Does not prove any convergence or divergence of the running maximum itself.
- Does not address sign or positivity of the underlying sequence.
- Does not extend the statement to continuous time or to infinite suprema.
- Does not supply bounds in norms other than the pointwise supremum.
Lean usage
theorem normalized_le_one (a : ℕ → ℝ) (n : ℕ) (h : 0 < a n) : normalized a n ≤ 1 := by unfold normalized; exact (div_le_one (runningMax_pos a n h)).mpr (runningMax_ge a n)formal statement (Lean)
38theorem runningMax_ge (a : ℕ → ℝ) (n : ℕ) :
39 a n ≤ runningMax a n := by
proof body
Term-mode proof.
40 unfold runningMax
41 apply Finset.le_sup'
42 simp
43
44/-- The running maximum is monotone non-decreasing. -/