The recursive state construction of the resisting coordinates, signs, and partial smooth oracles.

structure V7.Stage5AboveTwoLowerS5F.PrefixParameters (p : ℝ) (d T : ℕ) : Type

The fixed algorithm, kernel, scales, and horizon bounds used to build resisting prefixes.

• algorithm : DeterministicExactPairAlgorithm d

  The deterministic algorithm challenged by the prefix construction.

• kernel : SmoothingKernelData p d

  The smoothing kernel applied to each partial objective.

• delta : ℝ

  The offset between successive affine pieces.

• chi : ℝ

  The smoothing scale of the partial objectives.

• beta : ℝ

  The common scale multiplying the smooth oracle values and gradients.

• T_pos : 0 < T
• T_le_d : T ≤ d

def V7.Stage5AboveTwoLowerS5F.firstCoordinate {p : ℝ} {d T : ℕ} (P : PrefixParameters p d T) : Fin d

The zero coordinate, available because the positive horizon fits inside the dimension.

Equations

• V7.Stage5AboveTwoLowerS5F.firstCoordinate P = ⟨0, ⋯⟩

structure V7.Stage5AboveTwoLowerS5F.ResistingPrefixState (d : ℕ) : Type

The coordinates, signs, and observations selected by a finite resisting prefix.

• sigmaPrefix : List (Fin d)

  The previously selected distinct coordinates.

• xiPrefix : List ℝ

  The signs assigned to the selected coordinates.

• obsPrefix : List (Observation d)

  The observations already returned to the algorithm.

def V7.Stage5AboveTwoLowerS5F.initialState (d : ℕ) : ResistingPrefixState d

The empty state before any resisting coordinate or observation is chosen.

Equations

• V7.Stage5AboveTwoLowerS5F.initialState d = { sigmaPrefix := [], xiPrefix := [], obsPrefix := [] }

def V7.Stage5AboveTwoLowerS5F.priorSigma {p : ℝ} {d T : ℕ} (P : PrefixParameters p d T) (state : ResistingPrefixState d) (s : ℕ) : Fin d

A previously selected coordinate, with zero as the out-of-range default.

Equations

• V7.Stage5AboveTwoLowerS5F.priorSigma P state s = state.sigmaPrefix.getD s (V7.Stage5AboveTwoLowerS5F.firstCoordinate P)

noncomputable def V7.Stage5AboveTwoLowerS5F.stepQuery {p : ℝ} {d T : ℕ} (P : PrefixParameters p d T) (t : ℕ) (state : ResistingPrefixState d) : Point d

The next algorithm query, with the first query fixed at the origin.

Equations

• V7.Stage5AboveTwoLowerS5F.stepQuery P t state = if t = 0 then 0 else P.algorithm.nextQuery 0 state.obsPrefix

noncomputable def V7.Stage5AboveTwoLowerS5F.stepSigma {p : ℝ} {d T : ℕ} (P : PrefixParameters p d T) (t : ℕ) (state : ResistingPrefixState d) : Fin d

An unused coordinate maximizing the current query magnitude, chosen before the horizon.

Equations

• V7.Stage5AboveTwoLowerS5F.stepSigma P t state = if ht : t < T then Classical.choose ⋯ else V7.Stage5AboveTwoLowerS5F.firstCoordinate P

noncomputable def V7.Stage5AboveTwoLowerS5F.stepXi {p : ℝ} {d T : ℕ} (P : PrefixParameters p d T) (t : ℕ) (state : ResistingPrefixState d) : ℝ

The sign aligned with the current query at the newly selected coordinate.

Equations

• V7.Stage5AboveTwoLowerS5F.stepXi P t state = V7.Stage5AboveTwoLowerS5A2Envelope.resistingSign (V7.Stage5AboveTwoLowerS5F.stepQuery P t state (V7.Stage5AboveTwoLowerS5F.stepSigma P t state))

noncomputable def V7.Stage5AboveTwoLowerS5F.piece {p : ℝ} {d T : ℕ} (P : PrefixParameters p d T) (state : ResistingPrefixState d) (t i : ℕ) (x : Point d) : ℝ

An indexed signed-coordinate affine piece after appending the current resisting choice.

Equations

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

noncomputable def V7.Stage5AboveTwoLowerS5F.stepG {p : ℝ} {d T : ℕ} (P : PrefixParameters p d T) (t : ℕ) (state : ResistingPrefixState d) (x : Point d) : ℝ

The maximum of the affine pieces selected through the current step.

Equations

• V7.Stage5AboveTwoLowerS5F.stepG P t state x = (Finset.image (fun (i : ℕ) => V7.Stage5AboveTwoLowerS5F.piece P state t i x) (Finset.range (t + 1))).max' ⋯

noncomputable def V7.Stage5AboveTwoLowerS5F.stepH {p : ℝ} {d T : ℕ} (P : PrefixParameters p d T) (t : ℕ) (state : ResistingPrefixState d) (x : Point d) : ℝ

The resisting maximum combined with a radial term to ensure coercivity.

Equations

• V7.Stage5AboveTwoLowerS5F.stepH P t state x = max (V7.Stage5AboveTwoLowerS5F.stepG P t state x / 2) (V7.lpNorm p x - 3 / 2)

noncomputable def V7.Stage5AboveTwoLowerS5F.stepOracle {p : ℝ} {d T : ℕ} (P : PrefixParameters p d T) (t : ℕ) (state : ResistingPrefixState d) : PairOracle d

The scaled smooth oracle associated with the current regularized resisting objective.

Equations

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

noncomputable def V7.Stage5AboveTwoLowerS5F.advance {p : ℝ} {d T : ℕ} (P : PrefixParameters p d T) (t : ℕ) (state : ResistingPrefixState d) : ResistingPrefixState d

The prefix state after appending the selected coordinate, sign, and oracle observation.

Equations

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

noncomputable def V7.Stage5AboveTwoLowerS5F.prefixState {p : ℝ} {d T : ℕ} (P : PrefixParameters p d T) : ℕ → ResistingPrefixState d

The recursively generated resisting prefix state.

Equations

• V7.Stage5AboveTwoLowerS5F.prefixState P 0 = V7.Stage5AboveTwoLowerS5F.initialState d
• V7.Stage5AboveTwoLowerS5F.prefixState P t.succ = V7.Stage5AboveTwoLowerS5F.advance P t (V7.Stage5AboveTwoLowerS5F.prefixState P t)

noncomputable def V7.Stage5AboveTwoLowerS5F.query {p : ℝ} {d T : ℕ} (P : PrefixParameters p d T) (t : ℕ) : Point d

The query made at step t of the recursively generated resisting construction.

Equations

• V7.Stage5AboveTwoLowerS5F.query P t = V7.Stage5AboveTwoLowerS5F.stepQuery P t (V7.Stage5AboveTwoLowerS5F.prefixState P t)

noncomputable def V7.Stage5AboveTwoLowerS5F.sigma {p : ℝ} {d T : ℕ} (P : PrefixParameters p d T) (t : ℕ) : Fin d

The coordinate selected at step t of the resisting construction.

Equations

• V7.Stage5AboveTwoLowerS5F.sigma P t = V7.Stage5AboveTwoLowerS5F.stepSigma P t (V7.Stage5AboveTwoLowerS5F.prefixState P t)

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

The sign selected at step t of the resisting construction.

Equations

• V7.Stage5AboveTwoLowerS5F.xi P t = V7.Stage5AboveTwoLowerS5F.stepXi P t (V7.Stage5AboveTwoLowerS5F.prefixState P t)

noncomputable def V7.Stage5AboveTwoLowerS5F.partialG {p : ℝ} {d T : ℕ} (P : PrefixParameters p d T) (t : ℕ) : Point d → ℝ

The resisting affine maximum at prefix length t + 1.

Equations

• V7.Stage5AboveTwoLowerS5F.partialG P t = V7.Stage5AboveTwoLowerS5F.stepG P t (V7.Stage5AboveTwoLowerS5F.prefixState P t)

noncomputable def V7.Stage5AboveTwoLowerS5F.partialH {p : ℝ} {d T : ℕ} (P : PrefixParameters p d T) (t : ℕ) : Point d → ℝ

The regularized nonsmooth objective at prefix length t + 1.

Equations

• V7.Stage5AboveTwoLowerS5F.partialH P t = V7.Stage5AboveTwoLowerS5F.stepH P t (V7.Stage5AboveTwoLowerS5F.prefixState P t)

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

The scaled smoothed oracle at prefix length t + 1.

Equations

• V7.Stage5AboveTwoLowerS5F.partialOracle P t = V7.Stage5AboveTwoLowerS5F.stepOracle P t (V7.Stage5AboveTwoLowerS5F.prefixState P t)

@[simp]

theorem V7.Stage5AboveTwoLowerS5F.prefixState_zero {p : ℝ} {d T : ℕ} (P : PrefixParameters p d T) : prefixState P 0 = initialState d

@[simp]

theorem V7.Stage5AboveTwoLowerS5F.prefixState_succ {p : ℝ} {d T : ℕ} (P : PrefixParameters p d T) (t : ℕ) : prefixState P (t + 1) = advance P t (prefixState P t)

theorem V7.Stage5AboveTwoLowerS5F.prefix_lengths {p : ℝ} {d T : ℕ} (P : PrefixParameters p d T) (t : ℕ) : (prefixState P t).sigmaPrefix.length = t ∧ (prefixState P t).xiPrefix.length = t ∧ (prefixState P t).obsPrefix.length = t

theorem V7.Stage5AboveTwoLowerS5F.prefix_sigma_getD {p : ℝ} {d T : ℕ} {P : PrefixParameters p d T} {s t : ℕ} (hst : s < t) : (prefixState P t).sigmaPrefix.getD s (firstCoordinate P) = sigma P s

theorem V7.Stage5AboveTwoLowerS5F.prefix_xi_getD {p : ℝ} {d T : ℕ} {P : PrefixParameters p d T} {s t : ℕ} (hst : s < t) : (prefixState P t).xiPrefix.getD s 0 = xi P s