The squared-norm geometry, residual identities, and two-phase trial contracts for exponents below two.

noncomputable def V7.belowH {d : ℕ} (p : ℝ) (x : Point d) : ℝ

The scaled squared norm mirror potential for exponents between one and two.

Equations

• V7.belowH p x = 1 / (2 * (p - 1)) * V7.lpNorm p x ^ 2

noncomputable def V7.belowHstar {d : ℕ} (p : ℝ) (s : Point d) : ℝ

The conjugate scaled squared norm potential for the below-two geometry.

Equations

• V7.belowHstar p s = (p - 1) / 2 * V7.lpNorm (V7.conjugateExponent p) s ^ 2

noncomputable def V7.belowMirrorMap {d : ℕ} (p : ℝ) (s : Point d) : Point d

The scaled duality map giving the gradient of the below-two conjugate potential.

Equations

• V7.belowMirrorMap p s = (p - 1) • O3.dualityMap (V7.conjugateExponent p) s

noncomputable def V7.FunctionBregman {d : ℕ} (F : Point d → ℝ) (grad : Point d → Point d) (x y : Point d) : ℝ

The Bregman difference of a function and its specified gradient, based at y.

Equations

• V7.FunctionBregman F grad x y = F x - F y - V7.pairing (grad y) (x - y)

noncomputable def V7.FenchelConjugate {d : ℕ} (F : Point d → ℝ) (s : Point d) : ℝ

The real supremum of the affine dual pairings minus the objective.

Equations

• V7.FenchelConjugate F s = sSup {r : ℝ | ∃ (x : V7.Point d), r = V7.pairing s x - F x}

noncomputable def V7.BelowGeometryStatement : Prop

Source carrier for lem:belowgeometry (B02).

Equations

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

structure V7.BelowPrimalData (p : ℝ) (d n : ℕ) : Type

Oracle, minimizer, coefficients, iterates, and observations of a below-two primal phase.

• oracle : PairOracle d

  The value-gradient oracle of the primal phase.

• z : Point d

  The comparison minimizer used in the primal potential.

• fstar : ℝ

  The objective value at the comparison minimizer.

• u : ℕ → ℝ

  The quadratic cumulative weights of the below-two phase.

• dw : ℕ → ℝ

  The successive weight increments, with zero terminal increment.

• s : ℕ → Point d

  The accumulated dual vectors updated by weighted gradients.

• v : ℕ → Point d

  The mirror-map images of the accumulated dual vectors.

• x : ℕ → Point d

  The primal query iterates.

• trace : List (Observation d)

  The chronological oracle observations of the primal phase.

def V7.BelowPrimalDynamics {p : ℝ} {d n : ℕ} (data : BelowPrimalData p d n) : Prop

The prescribed below-two weights, initial state, and primal update recurrences.

Equations

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

def V7.BelowPrimalAssumptions {p : ℝ} {d n : ℕ} (data : BelowPrimalData p d n) : Prop

The below-two primal dynamics, convex gradient oracle, minimizer, guards, and exact trace.

Equations

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

noncomputable def V7.BelowPrimalStatement : Prop

Source carrier for lem:below-primal (B04--B05).

Equations

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

@[reducible, inline]

abbrev V7.VectorSeq (d : ℕ) : Type

A natural-number-indexed sequence of finite-dimensional real vectors.

Equations

• V7.VectorSeq d = (ℕ → V7.Point d)

@[reducible, inline]

abbrev V7.ScalarSeq : Type

A natural-number-indexed sequence of real coefficients.

Equations

• V7.ScalarSeq = (ℕ → ℝ)

@[reducible, inline]

abbrev V7.ScalarMatrix : Type

A real coefficient array indexed by two natural numbers.

Equations

• V7.ScalarMatrix = (ℕ → ℕ → ℝ)

noncomputable def V7.weightedSum {d : ℕ} (n : ℕ) (a : ScalarSeq) (X : VectorSeq d) : Point d

The coordinatewise weighted sum of the first n vectors.

Equations

• V7.weightedSum n a X j = ∑ i ∈ Finset.range n, a i * X i j

noncomputable def V7.BelowPrimalResidual {d : ℕ} (p : ℝ) (n : ℕ) (u _dw : ScalarSeq) (alpha : ScalarMatrix) (A B X : VectorSeq d) (Omega : Point d → ℝ) : ℝ

The primal energy residual combining gradient differences, mirror increments, and mixed pairings.

Equations

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

noncomputable def V7.BelowDualResidual {d : ℕ} (p : ℝ) (n : ℕ) (u : ScalarSeq) (alpha b : ScalarMatrix) (C D : VectorSeq d) (Omega : Point d → ℝ) : ℝ

The reversed dual energy residual with reciprocal weights and mixed pairings.

Equations

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

def V7.EvenIncrement {d : ℕ} (Omega : Point d → ℝ) : Prop

The increment potential is unchanged when its argument is negated.

Equations

• V7.EvenIncrement Omega = ∀ (x : V7.Point d), Omega (-x) = Omega x

def V7.BelowResidualMap {d : ℕ} (n : ℕ) (u : ScalarSeq) (A B C D : VectorSeq d) : Prop

The reverse-indexed gradient and mirror correspondence used in the residual identity.

Equations

• V7.BelowResidualMap n u A B C D = (C 0 = u n • A n ∧ (∀ i < n, C (n - i) - C (n - i - 1) = u i • (A i - A (i + 1))) ∧ ∀ i ≤ n, D i = B (n - i))

def V7.BelowXRecurrence {d : ℕ} (n : ℕ) (b : ScalarMatrix) (B X : VectorSeq d) : Prop

The primal iterate recurrence driven by coefficient-row differences.

Equations

• V7.BelowXRecurrence n b B X = (X 0 = B 0 ∧ ∀ k < n, X (k + 1) = X k - V7.weightedSum (k + 2) (b (k + 1)) B)

def V7.BelowCoefficientAssumptions (n : ℕ) (u dw : ScalarSeq) (alpha c b : ScalarMatrix) : Prop

The explicit quadratic weights and coefficient recurrences for the below-two residual identity.

Equations

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

def V7.SameOnHorizon {d : ℕ} (n : ℕ) (A B : VectorSeq d) : Prop

Two vector sequences agree through the inclusive horizon n.

Equations

• V7.SameOnHorizon n A B = ∀ k ≤ n, A k = B k

noncomputable def V7.BelowPointwiseResidualIdentityStatement : Prop

Source carrier for lem:below-identity (B06--B07).

Equations

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

structure V7.BelowDualData (p : ℝ) (d n : ℕ) : Type

Oracle, coefficients, gradients, iterates, and observations of a below-two dual phase.

• oracle : PairOracle d

  The value-gradient oracle of the below-two dual phase.

• u : ScalarSeq

  The cumulative weights underlying the reversed dual recurrence.

• dw : ScalarSeq

  The increments of the cumulative weight sequence.

• alpha : ScalarMatrix

  The coefficient matrix used for the dual query updates.

• c : ScalarMatrix

  The primal coefficient matrix associated with the dual phase.

• b : ScalarMatrix

  The coefficient-row differences used to accumulate dual gradients.

• G : VectorSeq d

  The gradients observed at the dual query points.

• q : VectorSeq d

  The dual phase query points.

• r : VectorSeq d

  The accumulated vectors to which the dual mirror map is applied.

• trace : List (Observation d)

  The chronological oracle observations of the dual phase.

def V7.BelowDualDynamics {p : ℝ} {d n : ℕ} (data : BelowDualData p d n) : Prop

The below-two coefficient conditions and reversed dual query and gradient recurrences.

Equations

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

def V7.BelowDualAssumptions {p : ℝ} {d n : ℕ} (data : BelowDualData p d n) : Prop

The below-two dual dynamics, convex gradient oracle, lower bound, guards, and exact trace.

Equations

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

noncomputable def V7.BelowTerminalGradientStatement : Prop

Source carrier for lem:below-dual (B07--B08).

Equations

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

noncomputable def V7.BelowGuardScalingStatement : Prop

Source carrier for lem:below-guard-scaling (B12), including the exact argument orientation in both normalized and physical Bregman remainders.

Equations

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

noncomputable def V7.normalizedPairOracle {d : ℕ} (c : Point d) (M D : ℝ) (oracle : PairOracle d) : PairOracle d

The oracle translated by c and rescaled by the distance and smoothness estimates.

Equations

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

structure V7.BelowTrialWitness (p : ℝ) (d : ℕ) : Type

The source's two finite phases, including their recurrences, the reused endpoint, and the fact that every physical iterate is in the actual report.

• n : ℕ

  The shared planned horizon of the two below-two phases.

• completedOne : ℕ

  The number of primal iterations actually completed.

• completedTwo : ℕ

  The number of dual iterations actually completed.

• phaseOne : BelowPrimalData p d self.n

  The recorded normalized primal phase execution.

• phaseTwo : BelowDualData p d self.n

  The recorded normalized dual phase execution.

• phaseTwoCenter : Point d

  The physical center of the translated dual phase.

def V7.BelowTrialOperationalContract {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (cached : CachedPair d) (oracle : PairOracle d) (report : TrialReport d) (w : BelowTrialWitness p d) : Prop

The horizon, normalization, phase execution, and report requirements of a below-two trial.

Equations

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

noncomputable def V7.BelowTrialStatement : Prop

Source carrier for prop:belowtrial (B01--B13), with the current no-log local count.

Equations

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