The 2 < p < infinity branch: exact restart and oracle-count ledger

This module proves the source-exact numerical and finite-trace facts that do not require the currently unresolved real-exponent p-uniform convexity theorem. In particular it records the corrected fact that one ceiling per restart contributes at most the number of restart levels, never Delta_0 / delta.

The public declarations O3.abovePhase and O3.aboveTrial are not asserted while O3.pUniformConvexity is unavailable. Their proofs use that theorem to derive both the estimate-sequence ledger and the restart gap/distance implication. This module does not replace it with a target-shaped assumption.

def O3.AboveTwoRegime (p : ℝ) : Prop

The genuine-real regime from TeX Section 3.

Equations

• O3.AboveTwoRegime p = (2 < p)

noncomputable def O3.aboveAlpha (p : ℝ) : ℝ

The exact trial exponent 2(p-1)/(p+2).

Equations

• O3.aboveAlpha p = 2 * (p - 1) / (p + 2)

theorem O3.aboveAlpha_pos {p : ℝ} (hp : AboveTwoRegime p) : 0 < aboveAlpha p

noncomputable def O3.aboveAP (p : ℝ) : ℝ

a_p = 2^(2-p)/p from the uniform-convexity inequality.

Equations

• O3.aboveAP p = 2 ^ (2 - p) / p

noncomputable def O3.aboveEta (p : ℝ) : ℝ

eta_p = 2^(-p-2).

Equations

• O3.aboveEta p = 2 ^ (-p - 2)

noncomputable def O3.aboveTheta (p : ℝ) : ℝ

vartheta_p = a_p eta_p.

Equations

• O3.aboveTheta p = O3.aboveAP p * O3.aboveEta p

theorem O3.aboveAP_pos {p : ℝ} (hp : AboveTwoRegime p) : 0 < aboveAP p

theorem O3.aboveEta_pos (p : ℝ) : 0 < aboveEta p

theorem O3.aboveTheta_pos {p : ℝ} (hp : AboveTwoRegime p) : 0 < aboveTheta p

theorem O3.aboveAP_lt_one {p : ℝ} (hp : AboveTwoRegime p) : aboveAP p < 1

theorem O3.aboveEta_lt_one {p : ℝ} (hp : AboveTwoRegime p) : aboveEta p < 1

theorem O3.aboveTheta_lt_one {p : ℝ} (hp : AboveTwoRegime p) : aboveTheta p < 1

noncomputable def O3.aboveGamma (p : ℝ) (n : ℕ) (B : ℝ) : ℝ

gamma = n^((p-2)/p) B^(2-p).

Equations

• O3.aboveGamma p n B = ↑n ^ ((p - 2) / p) * B ^ (2 - p)

theorem O3.aboveGamma_pos {p B : ℝ} {n : ℕ} (_hp : AboveTwoRegime p) (hn : 1 ≤ n) (hB : 0 < B) : 0 < aboveGamma p n B

noncomputable def O3.aboveStepWeight (M : ℝ) (t : ℕ) : ℝ

a_t=t/M for a natural iteration index.

Equations

• O3.aboveStepWeight M t = ↑t / M

noncomputable def O3.aboveAccumulatedWeight (M : ℝ) (t : ℕ) : ℝ

A_t=t(t+1)/(2M).

Equations

• O3.aboveAccumulatedWeight M t = ↑t * ↑(t + 1) / (2 * M)

@[simp]

theorem O3.aboveAccumulatedWeight_zero (M : ℝ) : aboveAccumulatedWeight M 0 = 0

theorem O3.aboveAccumulatedWeight_succ {M : ℝ} (hM : M ≠ 0) (t : ℕ) : aboveAccumulatedWeight M (t + 1) = aboveAccumulatedWeight M t + aboveStepWeight M (t + 1)

theorem O3.aboveAccumulatedWeight_pos {M : ℝ} {t : ℕ} (hM : 0 < M) (ht : 1 ≤ t) : 0 < aboveAccumulatedWeight M t

theorem O3.abovePhaseCoefficient_eq {M : ℝ} (hM : M ≠ 0) {t : ℕ} (ht : 1 ≤ t) : M * aboveStepWeight M t ^ 2 / (2 * aboveAccumulatedWeight M t) = ↑t / ↑(t + 1)

The source coefficient c_t=t/(t+1) and its bound by one.

theorem O3.abovePhaseCoefficient_le_one {t : ℕ} : ↑t / ↑(t + 1) ≤ 1

noncomputable def O3.aboveMu (p eps D : ℝ) : ℝ

mu=eta_p eps / D^(p-1).

Equations

• O3.aboveMu p eps D = O3.aboveEta p * eps / D ^ (p - 1)

noncomputable def O3.aboveRho (p eps : ℝ) : ℝ

rho=vartheta_p eps.

Equations

• O3.aboveRho p eps = O3.aboveTheta p * eps

theorem O3.aboveMu_pos {p eps D : ℝ} (_hp : AboveTwoRegime p) (heps : 0 < eps) (hD : 0 < D) : 0 < aboveMu p eps D

theorem O3.aboveRho_pos {p eps : ℝ} (hp : AboveTwoRegime p) (heps : 0 < eps) : 0 < aboveRho p eps

noncomputable def O3.aboveInitialLevel (M D : ℝ) : ℝ

Delta_0=M D^2.

Equations

• O3.aboveInitialLevel M D = M * D ^ 2

noncomputable def O3.aboveLevel (Delta0 : ℝ) (s : ℕ) : ℝ

Delta_s=2^(-s)Delta_0=Delta_0/2^s.

Equations

• O3.aboveLevel Delta0 s = Delta0 / 2 ^ s

noncomputable def O3.aboveTerminalLevel (rho M : ℝ) : ℝ

delta=rho^2/(8M).

Equations

• O3.aboveTerminalLevel rho M = rho ^ 2 / (8 * M)

theorem O3.aboveInitialLevel_pos {M D : ℝ} (hM : 0 < M) (hD : 0 < D) : 0 < aboveInitialLevel M D

theorem O3.aboveLevel_pos {Delta0 : ℝ} (hDelta0 : 0 < Delta0) (s : ℕ) : 0 < aboveLevel Delta0 s

@[simp]

theorem O3.aboveLevel_zero (Delta0 : ℝ) : aboveLevel Delta0 0 = Delta0

theorem O3.aboveLevel_succ (Delta0 : ℝ) (s : ℕ) : aboveLevel Delta0 (s + 1) = aboveLevel Delta0 s / 2

theorem O3.aboveTerminalLevel_pos {rho M : ℝ} (hrho : 0 < rho) (hM : 0 < M) : 0 < aboveTerminalLevel rho M

noncomputable def O3.aboveRestartCount (Delta0 delta : ℝ) : ℕ

The source restart count S = ceil(log_2 (Delta_0/delta)).

Equations

• O3.aboveRestartCount Delta0 delta = ⌈Real.logb 2 (Delta0 / delta)⌉₊

theorem O3.aboveRestartCount_pos {Delta0 delta : ℝ} (hdelta : 0 < delta) (horder : delta < Delta0) : 0 < aboveRestartCount Delta0 delta

theorem O3.aboveRestartCount_cast_le {Delta0 delta : ℝ} (hdelta : 0 < delta) (horder : delta ≤ Delta0) : ↑(aboveRestartCount Delta0 delta) ≤ Real.logb 2 (Delta0 / delta) + 1

Exact logarithmic ceiling bound; no Delta_0/delta overhead appears.

theorem O3.aboveLevel_restartCount_le {Delta0 delta : ℝ} (hDelta0 : 0 < Delta0) (hdelta : 0 < delta) : aboveLevel Delta0 (aboveRestartCount Delta0 delta) ≤ delta

The ceiling-defined restart count reaches the terminal level.

theorem O3.aboveRestartGap {Delta0 : ℝ} (gap : ℕ → ℝ) (hzero : gap 0 ≤ Delta0) (hstep : ∀ (s : ℕ), gap (s + 1) ≤ gap s / 2) (s : ℕ) : gap s ≤ aboveLevel Delta0 s

The restart induction: halving a proved gap at each successful level gives gap_s <= Delta_s. This is purely the scalar induction after the missing uniform-convexity and phase-rate steps have produced the halving premise.

theorem O3.aboveCeilingSum_le (S : ℕ) (work : Fin S → ℝ) (hwork : ∀ (s : Fin S), 0 ≤ work s) : ∑ s : Fin S, ↑⌈work s⌉₊ ≤ ∑ s : Fin S, work s + ↑S

The exact ceiling ledger: one ceiling at each of S levels contributes at most S above the corresponding real-valued work. This is the corrected overhead in TeX lines 484--492.

theorem O3.aboveGeometricSum_eq {c ratio : ℝ} (hratio : ratio ≠ 1) (S : ℕ) : ∑ s ∈ Finset.range S, c * ratio ^ s = c * ((ratio ^ S - 1) / (ratio - 1))

Exact finite geometric-sum identity used in the restart count.

theorem O3.aboveGeometricSum_le {c ratio : ℝ} (hc : 0 ≤ c) (hratio : 1 < ratio) (S : ℕ) : ∑ s ∈ Finset.range S, c * ratio ^ s ≤ c * ratio ^ S / (ratio - 1)

For ratio bigger than one, the geometric work is controlled by its end.

noncomputable def O3.aboveKappa (M D eps : ℝ) : ℝ

kappa=MD/eps.

Equations

• O3.aboveKappa M D eps = M * D / eps

theorem O3.aboveLevelRatio_eq {M D eps theta : ℝ} (hM : M ≠ 0) (heps : eps ≠ 0) (htheta : theta ≠ 0) : aboveInitialLevel M D / aboveTerminalLevel (theta * eps) M = 8 * aboveKappa M D eps ^ 2 / theta ^ 2

The source identity Delta_0/delta=8 kappa^2/vartheta_p^2. It is the exact input to the logarithmic restart-count statement.

theorem O3.aboveKappaThetaRatio_gt_one {p kappa : ℝ} (hp : AboveTwoRegime p) (hkappa : 1 < kappa) : 1 < 8 * kappa ^ 2 / aboveTheta p ^ 2

def O3.abovePhaseTrace {d N : ℕ} (oracle : PairOracle d) (y accelerated : Fin N → Vec d) : List (Observation d)

One accelerated iteration contributes its two exact pair observations.

Equations

• O3.abovePhaseTrace oracle y accelerated = List.flatMap (fun (i : Fin N) => [oracle.observe (y i), oracle.observe (accelerated i)]) (List.finRange N)

def O3.AboveObservationTraceExact {d : ℕ} (oracle : PairOracle d) (trace : List (Observation d)) : Prop

Every recorded response equals the oracle's exact value-gradient pair at its query point.

Equations

• O3.AboveObservationTraceExact oracle trace = ∀ observation ∈ trace, observation = oracle.observe observation.point

theorem O3.abovePhaseTrace_exact {d N : ℕ} (oracle : PairOracle d) (y accelerated : Fin N → Vec d) : AboveObservationTraceExact oracle (abovePhaseTrace oracle y accelerated)

@[simp]

theorem O3.abovePhaseTrace_length {d N : ℕ} (oracle : PairOracle d) (y accelerated : Fin N → Vec d) : (abovePhaseTrace oracle y accelerated).length = 2 * N

def O3.aboveRestartTrace {d S : ℕ} (oracle : PairOracle d) (horizons : Fin S → ℕ) (y accelerated : (s : Fin S) → Fin (horizons s) → Vec d) : List (Observation d)

All restart phases concatenated chronologically. horizons s is the actual natural iteration count at restart level s.

Equations

• O3.aboveRestartTrace oracle horizons y accelerated = List.flatMap (fun (s : Fin S) => O3.abovePhaseTrace oracle (y s) (accelerated s)) (List.finRange S)

theorem O3.aboveRestartTrace_exact {d S : ℕ} (oracle : PairOracle d) (horizons : Fin S → ℕ) (y accelerated : (s : Fin S) → Fin (horizons s) → Vec d) : AboveObservationTraceExact oracle (aboveRestartTrace oracle horizons y accelerated)

@[simp]

theorem O3.aboveRestartTrace_length {d S : ℕ} (oracle : PairOracle d) (horizons : Fin S → ℕ) (y accelerated : (s : Fin S) → Fin (horizons s) → Vec d) : (aboveRestartTrace oracle horizons y accelerated).length = (List.map (fun (s : Fin S) => 2 * horizons s) (List.finRange S)).sum

def O3.aboveTrialTrace {d S : ℕ} (oracle : PairOracle d) (horizons : Fin S → ℕ) (y accelerated : (s : Fin S) → Fin (horizons s) → Vec d) (extraction : Vec d) : List (Observation d)

Restart phases followed by the single counted extraction query.

Equations

• O3.aboveTrialTrace oracle horizons y accelerated extraction = O3.aboveRestartTrace oracle horizons y accelerated ++ [oracle.observe extraction]

theorem O3.aboveTrialTrace_exact {d S : ℕ} (oracle : PairOracle d) (horizons : Fin S → ℕ) (y accelerated : (s : Fin S) → Fin (horizons s) → Vec d) (extraction : Vec d) : AboveObservationTraceExact oracle (aboveTrialTrace oracle horizons y accelerated extraction)

theorem O3.aboveTrialTrace_callCount {d S : ℕ} (oracle : PairOracle d) (horizons : Fin S → ℕ) (y accelerated : (s : Fin S) → Fin (horizons s) → Vec d) (extraction : Vec d) : (aboveTrialTrace oracle horizons y accelerated extraction).length = (List.map (fun (s : Fin S) => 2 * horizons s) (List.finRange S)).sum + 1

Exact count: two calls per accelerated iteration and one extraction call.

theorem O3.aboveTrialTrace_extraction_queried {d S : ℕ} (oracle : PairOracle d) (horizons : Fin S → ℕ) (y accelerated : (s : Fin S) → Fin (horizons s) → Vec d) (extraction : Vec d) : extraction ∈ List.map Observation.point (aboveTrialTrace oracle horizons y accelerated extraction)