rescaleLength_tendsto_zero
If a sequence of reals diverges to positive infinity then its running-max rescaling factor converges to zero in the reals. Navier-Stokes analysts cite the result when constructing normalized ancient solutions from a hypothetical blow-up sequence. The proof is an epsilon-delta argument that invokes the running-max divergence lemma and then applies square-root monotonicity together with the metric definition of neighborhood convergence.
claimLet $a : ℕ → ℝ$ satisfy $a_n → +∞$ as $n → ∞$. Define the rescaling length by $ℓ(n) := 1 / √(sup_{k ≤ n} a_k)$. Then $ℓ(n) → 0$ as $n → ∞$.
background
The module implements the first step of the running-max normalization used in the Navier-Stokes regularity argument (NS Paper §3). Given a sequence $a_n$ of sup-norms that diverges, the running maximum is the monotone envelope $M(n) = sup_{k ≤ n} a_k$. The rescaling length is then the reciprocal square root $1/√M(n)$, which normalizes the vorticity so that its $L^∞$ norm is at most 1 on the rescaled coordinates. The local setting is pure real analysis: only monotonicity of the running max and the definition of convergence at infinity are required. The key upstream fact is the sibling lemma that the running max itself tends to infinity whenever the original sequence does.
proof idea
The tactic proof first calls the running-max divergence lemma to obtain that the running max tends to infinity. It then unfolds the metric definition of convergence to the zero neighborhood. For arbitrary ε > 0 it selects N large enough that the running max exceeds (1/ε)² + 1, after which positivity of the square root and the inequality √x > 1/ε together imply that the rescaled length is strictly less than ε for all n ≥ N.
why it matters in Recognition Science
The declaration supplies the vanishing of the rescaling factor required to extract a bounded ancient element from any hypothetical blow-up sequence. It therefore feeds the sibling statement that the normalized vorticity remains bounded by 1. In the Recognition Science framework this completes the normalization step that precedes the application of the Caffarelli-Kohn-Nirenberg-type regularity criterion. No open scaffolding remains inside the module.
scope and limits
- Does not assert existence of any diverging sequence of sup-norms.
- Does not address the Navier-Stokes equations themselves or any regularity criterion.
- Does not supply a convergence rate for the rescaling length.
- Does not extend to sequences that remain bounded.
formal statement (Lean)
102theorem rescaleLength_tendsto_zero (a : ℕ → ℝ) (h : Tendsto a atTop atTop) :
103 Tendsto (rescaleLength a) atTop (nhds 0) := by
proof body
Tactic-mode proof.
104 -- Strategy: for any ε > 0, get N so that runningMax a n > (1/ε)², then
105 -- sqrt(runningMax a n) > 1/ε, hence 1/sqrt(runningMax a n) < ε.
106 have h_max := runningMax_tendsto_atTop a h
107 rw [Metric.tendsto_nhds]
108 intro ε hε
109 have hie_pos : (0 : ℝ) < 1 / ε := by positivity
110 rw [Filter.tendsto_atTop_atTop] at h_max
111 obtain ⟨N, hN⟩ := h_max ((1 / ε) ^ 2 + 1)
112 rw [Filter.eventually_atTop]
113 refine ⟨N, fun n hn => ?_⟩
114 have hrun : (1 / ε) ^ 2 + 1 ≤ runningMax a n := hN n hn
115 have hrun_pos : (0 : ℝ) < runningMax a n := by linarith [sq_nonneg (1 / ε)]
116 have hsqrt_pos : (0 : ℝ) < Real.sqrt (runningMax a n) := Real.sqrt_pos.mpr hrun_pos
117 simp only [rescaleLength, Real.dist_eq, sub_zero,
118 abs_of_pos (div_pos one_pos hsqrt_pos)]
119 rw [div_lt_iff₀ hsqrt_pos]
120 have h_sqrt_bound : 1 / ε < Real.sqrt (runningMax a n) := by
121 rw [← Real.sqrt_sq hie_pos.le]
122 exact Real.sqrt_lt_sqrt (sq_nonneg _) (by linarith)
123 calc (1 : ℝ) = ε * (1 / ε) := by field_simp
124 _ < ε * Real.sqrt (runningMax a n) := by
125 exact mul_lt_mul_of_pos_left h_sqrt_bound hε
126
127/-! ## Properties of the Normalized Ancient Element -/
128
129/-- The normalized vorticity satisfies ‖ω̃ₙ‖ ≤ 1 for all n. -/