The recursive resisting prefixes assemble into valid completed lower-bound data.

theorem V7.Stage5AboveTwoLowerS5F.piece_eq_global {p : ℝ} {d T : ℕ} (P : PrefixParameters p d T) (t i : ℕ) (hit : i ≤ t) (x : Point d) : piece P (prefixState P t) t i x = xi P i * x (sigma P i) - ↑i * P.delta

theorem V7.Stage5AboveTwoLowerS5F.stepG_resisting {p : ℝ} {d T : ℕ} (P : PrefixParameters p d T) (t : ℕ) (x : Point d) : (∀ i ≤ t, xi P i * x (sigma P i) - ↑i * P.delta ≤ partialG P t x) ∧ ∃ i ≤ t, partialG P t x = xi P i * x (sigma P i) - ↑i * P.delta

theorem V7.Stage5AboveTwoLowerS5F.sigma_step_spec {p : ℝ} {d T : ℕ} (P : PrefixParameters p d T) {t : ℕ} (ht : t < T) : (∀ s < t, sigma P s ≠ sigma P t) ∧ ↑(sigma P t) < T ∧ ∀ (j : Fin d), ↑j < T → (∀ s < t, sigma P s ≠ j) → |query P t j| ≤ |query P t (sigma P t)|

theorem V7.Stage5AboveTwoLowerS5F.xi_step_spec {p : ℝ} {d T : ℕ} (P : PrefixParameters p d T) (t : ℕ) : (xi P t = 1 ∨ xi P t = -1) ∧ xi P t * query P t (sigma P t) = |query P t (sigma P t)|

noncomputable def V7.Stage5AboveTwoLowerS5F.completedOracle {p : ℝ} {d T : ℕ} (P : PrefixParameters p d T) : PairOracle d

The final scaled smooth oracle obtained from the last partial resisting objective.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def V7.Stage5AboveTwoLowerS5F.completionData {p : ℝ} {d T : ℕ} (P : PrefixParameters p d T) (Delta : ℝ) : LowerCompletionData p d T

The recursively constructed prefixes packaged as completed lower-bound data.

Equations

• One or more equations did not get rendered due to their size.

theorem V7.Stage5AboveTwoLowerS5F.completionData_assumptions {p : ℝ} {d T : ℕ} (P : PrefixParameters p d T) (Delta : ℝ) (hp : 2 < p) (hd : 2 ≤ d) (hkernel : SmoothingKernelAssumptions P.kernel) (hDelta : Delta = ↑T ^ (-1 / p)) (hdelta : P.delta = Delta / (2 * ↑T)) (hchi : P.chi = P.delta / 2) (hbeta : P.beta = P.chi / P.kernel.Mpd) : LowerCompletionAssumptions (completionData P Delta)