def accumulatedWeights (a : ℕ → ℝ) : ℕ → ℝ

Definition 6.53: the accumulated weights A_t = ∑_{k=0}^t a_k attached to the sequence a_t.

def WeightSequenceNotation.«termA[_](_)» : Lean.ParserDescr

theorem accumulatedWeights_apply (a : ℕ → ℝ) (t : ℕ) : accumulatedWeights a t = ∑ k ∈ Finset.range (t + 1), a k

Expanding A[a](t) gives the partial sum ∑_{k=0}^t a_k.

noncomputable def weightCoefficient (a : ℕ → ℝ) (t : ℕ) : ℝ

The normalized coefficients τ_t = a_{t+1} / A_{t+1} attached to the weights a_t.

def WeightSequenceNotation.«termτ[_](_)» : Lean.ParserDescr

theorem weightCoefficient_apply (a : ℕ → ℝ) (t : ℕ) : weightCoefficient a t = a (t + 1) / accumulatedWeights a (t + 1)

Expanding τ[a](t) gives the ratio a_{t+1} / A[a](t + 1).

noncomputable def linearOptimizationOracleErrorBound (V0 : ℝ) (a : ℕ → ℝ) (Gν D ν : ℝ) (t : ℕ) : ℝ

The Chapter 6 weighted oracle-error accumulation with initial term V₀, weights a_t, per-step coefficient G_ν, diameter bound D, and exponent ν. This is the canonical owner reused later by the source-facing error terms B_{ν,t} and C_{v,t}.

theorem linearOptimizationOracleErrorBound_def (V0 : ℝ) (a : ℕ → ℝ) (Gν D ν : ℝ) (t : ℕ) : linearOptimizationOracleErrorBound V0 a Gν D ν t = a 0 * V0 + (∑ k ∈ Finset.Icc 1 t, (a k).rpow (1 + ν) / (accumulatedWeights a k).rpow ν) * Gν * D.rpow (1 + ν)

Expanding linearOptimizationOracleErrorBound V₀ a G_ν D ν t gives the defining Chapter 6 weighted error formula with A_k = A[a](k).