The geometry, residual identities, phase bounds, and operational contracts for exponents above two.

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

The power mirror potential ‖x‖ₚ^p / p used for exponents above two.

Equations

• V7.aboveH p x = 1 / p * V7.lpNorm p x ^ p

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

The conjugate power potential with the Hölder-conjugate exponent.

Equations

• V7.aboveHstar p s = 1 / V7.conjugateExponent p * V7.lpNorm (V7.conjugateExponent p) s ^ V7.conjugateExponent p

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

The power duality map at the Hölder-conjugate exponent.

Equations

• V7.aboveMirrorMap p s = O3.powerDualityMap (V7.conjugateExponent p) s

noncomputable def V7.AboveGeometryStatement : Prop

The conjugacy, gradient, uniform convexity, and Bregman identities for the above-two geometry.

Equations

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

noncomputable def V7.aboveUniformConstant (p : ℝ) : ℝ

The uniform convexity constant of the power mirror potential.

Equations

• V7.aboveUniformConstant p = 2 ^ (2 - p) / p

noncomputable def V7.aboveErrorPower (p : ℝ) : ℝ

The exponent in the accumulated above-two residual error.

Equations

• V7.aboveErrorPower p = p / (p - 2)

noncomputable def V7.aboveErrorConstant (p : ℝ) : ℝ

The coefficient of the error bound obtained from the above-two mixed residual.

Equations

• V7.aboveErrorConstant p = (p - 2) / (2 * p) * (p * V7.aboveUniformConstant p) ^ (-2 / (p - 2))

noncomputable def V7.aboveBudgetConstant (p : ℝ) : ℝ

The error constant after bounding the squared weight increments by their growth rate.

Equations

• V7.aboveBudgetConstant p = 4 ^ V7.aboveErrorPower p * V7.aboveErrorConstant p

noncomputable def V7.aboveBudgetExponent (p : ℝ) : ℝ

The exponent relating an above-two error budget to the coefficient scale.

Equations

• V7.aboveBudgetExponent p = (p - 2) / p

noncomputable def V7.aboveGrowthConstant (p : ℝ) : ℝ

The coefficient of the terminal weight in terms of the error budget and horizon.

Equations

• V7.aboveGrowthConstant p = (2 * V7.aboveBudgetConstant p) ^ (-V7.aboveBudgetExponent p)

noncomputable def V7.aboveHp (p : ℝ) : ℝ

The exponent-dependent constant used to choose the primal trial horizon.

Equations

• V7.aboveHp p = 3 * p ^ V7.aboveBudgetExponent p / (2 * p * V7.aboveGrowthConstant p)

noncomputable def V7.aboveJp (p : ℝ) : ℝ

The exponent-dependent constant used to choose the dual trial horizon.

Equations

• V7.aboveJp p = 2 * V7.conjugateExponent p ^ (1 + V7.aboveBudgetExponent p) / V7.aboveGrowthConstant p

noncomputable def V7.aboveGamma (p eta : ℝ) (n : ℕ) : ℝ

The weight scale chosen from the error budget and iteration horizon.

Equations

• V7.aboveGamma p eta n = (eta / (2 * V7.aboveBudgetConstant p * ↑n)) ^ V7.aboveBudgetExponent p

noncomputable def V7.aboveErrorSum (p : ℝ) (n : ℕ) (u dw : ScalarSeq) : ℝ

The accumulated above-two residual error for a weight sequence and its increments.

Equations

• V7.aboveErrorSum p n u dw = V7.aboveErrorConstant p * ∑ k ∈ Finset.range n, (dw k ^ 2 / u k) ^ V7.aboveErrorPower p

noncomputable def V7.AboveWeightErrorBalanceStatement : Prop

Quadratic trial weights meet the error budget and have the stated terminal growth.

Equations

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

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

The primal residual for above-two geometry, expressed through the common residual formula.

Equations

• V7.AbovePrimalResidual p n u alpha A B X Omega = V7.BelowPrimalResidual p n u (fun (x : ℕ) => 0) alpha A B X Omega

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

The dual residual for above-two geometry, expressed through the common residual formula.

Equations

• V7.AboveDualResidual p n u alpha b C D Omega = V7.BelowDualResidual p n u alpha b C D Omega

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

The weight, increment, matrix recurrence, row-sum, and support conditions for an above-two phase.

Equations

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

noncomputable def V7.AbovePointwiseResidualIdentityStatement : Prop

Source carrier for lem:above-pointwise (A05).

Equations

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

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

Oracle, coefficients, iterates, and observations of an above-two primal phase.

• oracle : PairOracle d

  The value-gradient oracle used by the primal phase.

• fstar : ℝ

  The proposed minimum value of the objective.

• u : ScalarSeq

  The cumulative weights of the primal phase.

• dw : ScalarSeq

  The successive weight increments, with zero terminal increment.

• alpha : ScalarMatrix

  The matrix selecting the weighted gradient contribution at each step.

• c : ScalarMatrix

  The coefficients expressing each primal iterate in the mirror iterates.

• b : ScalarMatrix

  The successive differences of the primal coefficient rows.

• s : VectorSeq d

  The accumulated dual vectors updated by weighted gradients.

• v : VectorSeq d

  The mirror-map images of the accumulated dual vectors.

• x : VectorSeq d

  The primal query iterates.

• trace : List (Observation d)

  The chronological value-gradient observations of the phase.

def V7.AbovePrimalPhaseDynamics {p : ℝ} {d n : ℕ} (data : AbovePrimalPhaseData p d n) : Prop

The above-two primal coefficient conditions, initial state, and step recurrences.

Equations

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

def V7.AbovePrimalPhaseAssumptions {p : ℝ} {d n : ℕ} (data : AbovePrimalPhaseData p d n) : Prop

The primal dynamics, convex gradient oracle, attained minimum, guards, and exact query trace.

Equations

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

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

Oracle, coefficients, iterates, and observations of an above-two dual phase.

• oracle : PairOracle d

  The value-gradient oracle used by the dual phase.

• u : ScalarSeq

  The cumulative weights underlying the reversed dual recurrence.

• dw : ScalarSeq

  The weight increments underlying the reversed dual recurrence.

• 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.

• r : VectorSeq d

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

• q : VectorSeq d

  The dual phase query points.

• trace : List (Observation d)

  The chronological value-gradient observations of the dual phase.

def V7.AboveDualPhaseDynamics {p : ℝ} {d n : ℕ} (data : AboveDualPhaseData p d n) : Prop

The above-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.AboveDualPhaseAssumptions {p : ℝ} {d n : ℕ} (data : AboveDualPhaseData p d n) : Prop

The dual dynamics, convex gradient oracle, lower bound, accepted guards, and exact trace.

Equations

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

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

The two phase executions and numerical parameters witnessing an above-two trial.

• nF : ℕ

  The planned number of primal phase iterations.

• nD : ℕ

  The planned number of dual phase iterations.

• completedF : ℕ

  The number of primal iterations actually completed.

• completedD : ℕ

  The number of dual iterations actually completed.

• etaF : ℝ

  The primal phase error budget.

• etaD : ℝ

  The dual phase error budget.

• gammaF : ℝ

  The scale of the primal phase weights.

• gammaD : ℝ

  The scale of the dual phase weights.

• phaseOne : AbovePrimalPhaseData p d self.nF

  The recorded primal phase execution.

• phaseTwo : AboveDualPhaseData p d self.nD

  The recorded dual phase execution.

• phaseTwoCenter : Point d

  The center used to translate the dual phase back to physical coordinates.

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

The horizon, normalization, phase execution, and report requirements of an above-two trial.

Equations

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

noncomputable def V7.AboveTrialStatement : Prop

Source carrier for prop:abovetrial (A01--A12), with the current p/(p+2) exponent and endpoint reuse.

Equations

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