Diagonal cutoff scales from actual logarithmic limits

This module proves the numerical cutoff-selection step in Lemma 11.3 of the candidate manuscript. The decay of powers times logarithms is proved using Mathlib's exponential asymptotic, not assumed as a cutoff-schedule hypothesis. The resulting schedule enforces every requested finite collection of jet bounds. It does not construct the analytic increments or prove their PDE estimates.

noncomputable def NavierStokes.DiagonalScale.logPowerWeight (C p r q : ℝ) : ℝ

The scalar expression whose smallness is needed at each correction stage.

Equations

• NavierStokes.DiagonalScale.logPowerWeight C p r q = C * (1 + |Real.log q|) ^ p * q ^ r

theorem NavierStokes.DiagonalScale.tendsto_logPowerWeight (C p r : ℝ) (hr : 0 < r) : Filter.Tendsto (logPowerWeight C p r) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Any positive real power beats any fixed real logarithmic power at zero.

theorem NavierStokes.DiagonalScale.absorb_logarithmic_weight (C p g L q ε : ℝ) (hq : 0 < q) (hsmall : |logPowerWeight C p (g / 2) q| ≤ ε) : |C * (1 + |Real.log q|) ^ p * q ^ (g - L)| ≤ ε * q ^ (g / 2 - L)

Absorbing half the positive power into the chosen small coefficient gives exactly the stage bound used in the manuscript's tail estimate.

theorem NavierStokes.DiagonalScale.exists_integer_scale {ι : Type u_1} (s : Finset ι) (C p : ι → ℝ) (r ε : ℝ) (hr : 0 < r) (hε : 0 < ε) : ∃ (a : ℕ), 0 < a ∧ ∀ i ∈ s, ∀ (q : ℝ), 0 < q → q ≤ 1 / ↑a → |logPowerWeight (C i) (p i) r q| ≤ ε

A common integer scale controls an arbitrary finite family, uniformly on the entire punctured interval through its reciprocal.

def NavierStokes.DiagonalScale.doublingEnvelope (b : ℕ → ℕ) : ℕ → ℕ

A recursive integer sequence dominating prescribed local scales and at least doubling on every step.

Equations

• NavierStokes.DiagonalScale.doublingEnvelope b 0 = max 1 (b 0)
• NavierStokes.DiagonalScale.doublingEnvelope b n.succ = max (b (n + 1)) (2 * NavierStokes.DiagonalScale.doublingEnvelope b n)

theorem NavierStokes.DiagonalScale.doublingEnvelope_ge (b : ℕ → ℕ) (n : ℕ) : b n ≤ doublingEnvelope b n

theorem NavierStokes.DiagonalScale.doublingEnvelope_growth (b : ℕ → ℕ) (n : ℕ) : 2 * doublingEnvelope b n ≤ doublingEnvelope b (n + 1)

theorem NavierStokes.DiagonalScale.doublingEnvelope_pos (b : ℕ → ℕ) (n : ℕ) : 0 < doublingEnvelope b n

theorem NavierStokes.DiagonalScale.doublingEnvelope_lower_bound (b : ℕ → ℕ) (n : ℕ) : n + 1 ≤ doublingEnvelope b n

theorem NavierStokes.DiagonalScale.doublingEnvelope_strictMono (b : ℕ → ℕ) : StrictMono (doublingEnvelope b)

theorem NavierStokes.DiagonalScale.doublingEnvelope_reciprocal_eventually_small (b : ℕ → ℕ) (q : ℝ) (hq : 0 < q) : ∃ (N : ℕ), ∀ j ≥ N, 1 / ↑(doublingEnvelope b j) < q

Consequently only finitely many cutoff supports can reach a fixed q > 0.

theorem NavierStokes.DiagonalScale.doublingEnvelope_finite_active (b : ℕ → ℕ) (q : ℝ) (hq : 0 < q) : {j : ℕ | q ≤ 1 / ↑(doublingEnvelope b j)}.Finite

The indices whose numerical cutoff support reaches a fixed positive scale form a finite set. This is the local-finiteness input, before introducing fields.

theorem NavierStokes.DiagonalScale.exists_diagonal_scales (C p : ℕ → ℕ → ℝ) (g : ℕ → ℝ) (hg : ∀ (j : ℕ), 1 ≤ j → 0 < g j) (B : ℕ) : ∃ (a : ℕ → ℕ), B ≤ a 0 ∧ (∀ (j : ℕ), 0 < a j) ∧ (∀ (j : ℕ), 2 * a j ≤ a (j + 1)) ∧ StrictMono a ∧ (∀ (q : ℝ), 0 < q → ∃ (N : ℕ), ∀ j ≥ N, 1 / ↑(a j) < q) ∧ ∀ (j : ℕ), 1 ≤ j → ∀ m ≤ j + 2, ∀ (q : ℝ), 0 < q → q ≤ 1 / ↑(a j) → |logPowerWeight (C j m) (p j m) (g j / 2) q| ≤ (1 / 2) ^ j

The numerical cutoff schedule of Lemma 11.3. Stage zero is exempt from a positive decay exponent, as in the source. Every positive stage enforces all jet requirements m ≤ j+2, with one schedule shared by all those requirements. The optional integer B gives an arbitrary lower bound on the initial scale.

theorem NavierStokes.DiagonalScale.dyadic_tail_sum (J : ℕ) (A : ℝ) : ∑' (n : ℕ), (1 / 2) ^ (J + 1 + n) * A = (1 / 2) ^ J * A

The exact dyadic tail used to sum the scalar majorants.

theorem NavierStokes.DiagonalScale.weighted_tail_bound (g : ℕ → ℝ) (hg : Monotone g) (L q : ℝ) (hq : 0 < q) (hq1 : q ≤ 1) (J : ℕ) : (Summable fun (n : ℕ) => (1 / 2) ^ (J + 1 + n) * q ^ (g (J + 1 + n) / 2 - L)) ∧ ∑' (n : ℕ), (1 / 2) ^ (J + 1 + n) * q ^ (g (J + 1 + n) / 2 - L) ≤ (1 / 2) ^ J * q ^ (g (J + 1) / 2 - L)

The scalar tail bound printed in Lemma 11.3, valid uniformly for every 0 < q ≤ 1. The sum indexes the tail by j = J + 1 + n.

theorem NavierStokes.DiagonalScale.exists_uniform_tail_order (g : ℕ → ℝ) (hg : Monotone g) (hgtop : Filter.Tendsto g Filter.atTop Filter.atTop) (L N : ℝ) (m : ℕ) : ∃ (J : ℕ), m ≤ J ∧ ∀ (q : ℝ), 0 < q → q ≤ 1 → ∑' (n : ℕ), (1 / 2) ^ (J + 1 + n) * q ^ (g (J + 1 + n) / 2 - L) ≤ (1 / 2) ^ J * q ^ N

If the prescribed order gains increase without bound, a single tail index works for an arbitrary target power and for every q in the unit interval. This concerns scalar majorants; it does not assert flatness of a PDE residual.