noncomputable def uncertainEnvironmentBarrierStepObjective {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {P : Set E} {N : ℕ} (F : E → ℝ) (ψ : Fin N → E → ℝ) (ν : NNRealˣ) (x0 : ↑P) (history : Fin (N + 1) → ↑P) (k : Fin N) : E → ℝ

The step objective optimized at stage k : Fin N in the uncertain-environment barrier method. The finite sum is taken over the initial segment { i : Fin N | i ≤ k } = Finset.Iic k, so only the source-defined payoff data ψ₀, …, ψ_k and iterate history x₀, …, x_k enter.

theorem uncertainEnvironmentBarrierStepObjective_apply {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {P : Set E} {N : ℕ} (F : E → ℝ) (ψ : Fin N → E → ℝ) (ν : NNRealˣ) (x0 : ↑P) (history : Fin (N + 1) → ↑P) (k : Fin N) (x : E) : uncertainEnvironmentBarrierStepObjective F ψ ν x0 history k x = 1 / (↑↑k + 1) * ∑ i ∈ Finset.Iic k, inner ℝ (barrierSubgradientDirection (ψ i) ↑(history i.castSucc)) (x - ↑(history i.castSucc)) - barrierSubgradientPenaltyWeight ν ↑k * (F x - F ↑x0)

Evaluating uncertainEnvironmentBarrierStepObjective F ψ ν x0 history k recovers the finite-horizon Algorithm 7.16 objective at stage k.

structure UncertainEnvironmentBarrierSubgradientMethod {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (P : Set E) (F : E → ℝ) (ν : NNRealˣ) (N : ℕ) (ψ : Fin N → E → ℝ) (x0 : ↑P) : Type u

Algorithm 7.16: given an initial point x₀ ∈ P, a finite-horizon payoff family ψ₀, …, ψ_{N-1}, and a horizon N, an uncertain-environment barrier subgradient method is a finite run x₀, …, x_N such that for each stage k = 0, …, N - 1, the next iterate x_{k+1} maximizes the displayed averaged relative-scale model with barrier penalty over P. The self-concordant-barrier hypothesis on F is part of later theorem layers, not primitive run data.

• ψ_differentiableOn (i : Fin N) : DifferentiableOn ℝ (ψ i) P

  Each payoff ψ_i from the finite horizon is differentiable on the feasible set P.

• ψ_pos (i : Fin N) {x : E} (hx : x ∈ P) : 0 < ψ i x

  Each payoff ψ_i from the finite horizon is strictly positive on the feasible set P.

• iterate : Fin (N + 1) → ↑P

  The finite feasible iterate trace x₀, …, x_N.

• iterate_zero : self.iterate 0 = x0

  The zeroth iterate is the prescribed initial point x₀.

• step_isMax (k : Fin N) : IsMaxOn (uncertainEnvironmentBarrierStepObjective F ψ ν x0 self.iterate k) P ↑(self.iterate k.succ)

  For each stage k : Fin N, the successor iterate x_{k+1} maximizes the averaged relative-scale objective with barrier penalty over P. Feasibility is carried by the subtype trace iterate : Fin (N + 1) → P.

@[implicit_reducible]

instance UncertainEnvironmentBarrierSubgradientMethod.instCoeFunForallFinHAddNatOfNat {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {P : Set E} {F : E → ℝ} {ν : NNRealˣ} {N : ℕ} {ψ : Fin N → E → ℝ} {x0 : ↑P} : CoeFun (UncertainEnvironmentBarrierSubgradientMethod P F ν N ψ x0) fun (x : UncertainEnvironmentBarrierSubgradientMethod P F ν N ψ x0) => Fin (N + 1) → E

A run of Algorithm 7.16 can be used as its finite iterate trace x₀, …, x_N.

theorem UncertainEnvironmentBarrierSubgradientMethod.x0_mem {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {P : Set E} {F : E → ℝ} {ν : NNRealˣ} {N : ℕ} {ψ : Fin N → E → ℝ} {x0 : ↑P} (_method : UncertainEnvironmentBarrierSubgradientMethod P F ν N ψ x0) : ↑x0 ∈ P

The prescribed initial point belongs to the feasible set P.

noncomputable def UncertainEnvironmentBarrierSubgradientMethod.stepObjective {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {P : Set E} {F : E → ℝ} {ν : NNRealˣ} {N : ℕ} {ψ : Fin N → E → ℝ} {x0 : ↑P} (method : UncertainEnvironmentBarrierSubgradientMethod P F ν N ψ x0) (k : Fin N) : E → ℝ

The step objective attached to an uncertain-environment barrier method at stage k : Fin N.

theorem UncertainEnvironmentBarrierSubgradientMethod.stepObjective_def {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {P : Set E} {F : E → ℝ} {ν : NNRealˣ} {N : ℕ} {ψ : Fin N → E → ℝ} {x0 : ↑P} (method : UncertainEnvironmentBarrierSubgradientMethod P F ν N ψ x0) (k : Fin N) : method.stepObjective k = uncertainEnvironmentBarrierStepObjective F ψ ν x0 method.iterate k

Expanding method.stepObjective k gives the Algorithm 7.16 objective evaluated on the finite iterate trace of method.

theorem UncertainEnvironmentBarrierSubgradientMethod.iterate_mem {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {P : Set E} {F : E → ℝ} {ν : NNRealˣ} {N : ℕ} {ψ : Fin N → E → ℝ} {x0 : ↑P} (method : UncertainEnvironmentBarrierSubgradientMethod P F ν N ψ x0) (k : Fin (N + 1)) : (fun (k : Fin (N + 1)) => ↑(method.iterate k)) k ∈ P

Every iterate of an uncertain-environment barrier method belongs to the feasible set P.

theorem UncertainEnvironmentBarrierSubgradientMethod.iterates_succ_mem {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {P : Set E} {F : E → ℝ} {ν : NNRealˣ} {N : ℕ} {ψ : Fin N → E → ℝ} {x0 : ↑P} (method : UncertainEnvironmentBarrierSubgradientMethod P F ν N ψ x0) (k : Fin N) : (fun (k : Fin (N + 1)) => ↑(method.iterate k)) k.succ ∈ P

Every successor iterate x_{k+1} belongs to the feasible set P.

theorem UncertainEnvironmentBarrierSubgradientMethod.step_isMaxOn {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {P : Set E} {F : E → ℝ} {ν : NNRealˣ} {N : ℕ} {ψ : Fin N → E → ℝ} {x0 : ↑P} (method : UncertainEnvironmentBarrierSubgradientMethod P F ν N ψ x0) (k : Fin N) : IsMaxOn (method.stepObjective k) P ((fun (k : Fin (N + 1)) => ↑(method.iterate k)) k.succ)

For each stage k : Fin N, the successor iterate x_{k+1} maximizes the Algorithm 7.16 step objective over P.