the later start m₊(R) and the exponent p₊ (2), §4, §6 item 11. The relative induction

of starts at m₊(R) = 1 + min {j ≥ 1 : ε_j^{1+γ/2-δ} ≤ R}; here laterStart β Λ R is the index j = m₊(R) - 1. This module proves that the minimum exists, that every m ≥ m₊(R) also satisfies the original mTheta0 bound, the exponent facts 0 < p₊ < 2, the radius bound for smooth analytic data, and the lower bound ε_j^{β+γ} ≥ 2^{-(β+γ)} R^{p₊} for j ≥ 2.

noncomputable def AVenhance.Infra.Section5.RelativeError.laterStart (β : ℝ) (Λ : ℕ) (R : ℝ) : ℕ

m₊(R) − 1: the least j ≥ 1 with ε_j^{1+γ/2−δ} ≤ R ((1)).

Equations

• AVenhance.Infra.Section5.RelativeError.laterStart β Λ R = sInf {j : ℕ | 1 ≤ j ∧ AVenhance.epsilon β Λ j ^ (1 + AVenhance.gamma β / 2 - AVenhance.delta β) ≤ R}

noncomputable def AVenhance.Infra.Section5.RelativeError.pPlus (β : ℝ) : ℝ

p₊ = q(β+γ)/(1+γ/2−δ) ((2)).

Equations

• AVenhance.Infra.Section5.RelativeError.pPlus β = AVenhance.q β * (β + AVenhance.gamma β) / (1 + AVenhance.gamma β / 2 - AVenhance.delta β)

theorem AVenhance.Infra.Section5.RelativeError.LaterStart.eps_pos {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {m : ℕ} : 0 < epsilon β Λ m

theorem AVenhance.Infra.Section5.RelativeError.LaterStart.eps_le_one {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {m : ℕ} : epsilon β Λ m ≤ 1

theorem AVenhance.Infra.Section5.RelativeError.later_exponent_pos {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : 0 < 1 + gamma β / 2 - delta β

The exponent 1 + γ/2 − δ is positive on the range.

theorem AVenhance.Infra.Section5.RelativeError.later_exponent_le {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : 1 + gamma β / 2 - delta β ≤ 1 + gamma β / 2

The exponent 1 + γ/2 − δ is at most 1 + γ/2.

theorem AVenhance.Infra.Section5.RelativeError.epsilon_antitone {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {n m : ℕ} (hnm : n ≤ m) : epsilon β Λ m ≤ epsilon β Λ n

The length scales are antitone in the index.

theorem AVenhance.Infra.Section5.RelativeError.LaterStart.rpow_neg_nat_rpow {Λ : ℝ} (hΛ : 0 < Λ) (j : ℕ) (e : ℝ) : (Λ ^ (-↑j)) ^ e = (Λ ^ (-e)) ^ j

(Λ^{-j})^e = (Λ^{-e})^j, used for the decay of ε_j^e.

theorem AVenhance.Infra.Section5.RelativeError.laterStart_set_nonempty {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {R : ℝ} (hR : 0 < R) : {j : ℕ | 1 ≤ j ∧ epsilon β Λ j ^ (1 + gamma β / 2 - delta β) ≤ R}.Nonempty

The defining set of laterStart is nonempty.

theorem AVenhance.Infra.Section5.RelativeError.laterStart_isLeast {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {R : ℝ} (hR : 0 < R) : IsLeast {j : ℕ | 1 ≤ j ∧ epsilon β Λ j ^ (1 + gamma β / 2 - delta β) ≤ R} (laterStart β Λ R)

theorem AVenhance.Infra.Section5.RelativeError.later_scale_of_le {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {R : ℝ} (hR : 0 < R) {m : ℕ} (hm : laterStart β Λ R + 1 ≤ m) : epsilon β Λ (m - 1) ^ (1 + gamma β / 2 - delta β) ≤ R ∧ mTheta0 β Λ R ≤ m

Every level m ≥ m₊(R) satisfies the later scale condition and the original mTheta0 bound.

The exponent p₊ < 2

theorem AVenhance.Infra.Section5.RelativeError.LaterStart.pPlus_poly {q : ℝ} (h1 : 1 < q) (h2 : q ≤ 3 / 2) : 0 < 23 * q ^ 2 + 6 * q - 5 - 16 * q ^ 3

The cubic certificate behind p₊ < 2: positive on (1, 3/2].

theorem AVenhance.Infra.Section5.RelativeError.LaterStart.pPlus_ineq_aux {q β γ δ : ℝ} (h1 : 1 < q) (h2 : q ≤ 3 / 2) (hβ : β * (4 * q - 1) = 4 * q) (hγ : γ * (q + 1) = (q - 1) * β) (hδ : δ * (4 * (q + 1) * (4 * q - 1)) = (q - 1) ^ 2) : q * (β + γ) < 2 * (1 + γ / 2 - δ)

q(β+γ) < 2(1+γ/2−δ) as a statement about abstract reals satisfying the defining relations of β, γ, δ in terms of q ∈ (1, 3/2].

theorem AVenhance.Infra.Section5.RelativeError.pPlus_pos_lt_two {β : ℝ} (hβ : 6 / 5 ≤ β) (hβ' : β < 4 / 3) : 0 < pPlus β ∧ pPlus β < 2

Radius bound

theorem AVenhance.Infra.Section5.RelativeError.analytic_radius_le {R : ℝ} (hR : 0 < R) {g : Homogenization.Vec 2 → ℝ} (hg : ContDiff ℝ (↑⊤) g) (hgp : IsZ2Periodic g) (hgm : Homogenization.MeanZeroOn unitCube g) (hga : IsThetaAnalytic R g) (hg0 : 0 < l2NormSq g) : R ≤ 1 / (√2 * Real.pi)

Smooth analytic nonzero data have R ≤ 1/(√2 π) (Poincaré + the n = 1 analytic bound).

The lower bound for ε_j^{β+γ} at the later start

theorem AVenhance.Infra.Section5.RelativeError.rpow_chain_lower {R y z e q h : ℝ} (hR : 0 < R) (hy : 0 < y) (he : 0 < e) (hq : 0 < q) (hh : 0 < h) (hRy : R < y ^ e) (hz : y ^ q / 2 ≤ z) : (1 / 2) ^ h * R ^ (q * h / e) ≤ z ^ h

Pure-real chain: R < y^e, y^q/2 ≤ z give 2^{-h} R^{qh/e} ≤ z^h.

theorem AVenhance.Infra.Section5.RelativeError.later_eps_pow_lower {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {R : ℝ} (hR : 0 < R) (hj : 2 ≤ laterStart β Λ R) : (1 / 2) ^ (β + gamma β) * R ^ pPlus β ≤ epsilon β Λ (laterStart β Λ R) ^ (β + gamma β)

For j = laterStart ≥ 2, minimality gives 2^{-(β+γ)} R^{p₊} ≤ ε_j^{β+γ}.