@[reducible, inline]

abbrev KelleyAmbient (n : ℕ) : Type

Helper for Theorem 3.56: the source-facing ambient space ℝ × ℝ^(n - 1) of the Kelley hard instance.

theorem origin_mem_kelleyCompleteArgmin {n : ℕ} : 0 ∈ constrainedArgmin kelleyCompleteFeasibleSet kelleyCompleteObjective

The origin is a constrained minimizer of the complete-data Kelley objective on the explicit feasible set Q.

structure KelleyCompleteFirstOrderExecution (n : ℕ) : Type

A source-facing execution record for Theorem 3.56.

• z : ℕ → KelleyAmbient n

def KelleyCompleteFirstOrderExecution.HasGapLowerBound {n : ℕ} (execution : KelleyCompleteFirstOrderExecution n) : Prop

The source-facing execution stays in the complete-data feasible set Q and satisfies the displayed geometric objective-gap lower bound at every iterate.

def KelleyCompleteFirstOrderExecution.HasCallLowerBound {n : ℕ} (execution : KelleyCompleteFirstOrderExecution n) : Prop

The source-facing execution satisfies the displayed oracle-call lower bound whenever an iterate reaches an ε-accurate objective value.

theorem kelleyComplete_optimality {n : ℕ} (hn : 1 ≤ n) : kelleyCompleteObjective 0 = 0 ∧ 0 ∈ constrainedArgmin kelleyCompleteFeasibleSet kelleyCompleteObjective

The optimality clause for the complete-data Kelley instance.

structure KelleyCompleteLowerBoundWitness (n : ℕ) : Prop

A bundled witness for the nondegenerate Kelley lower-bound clause.

• exists_execution : ∃ (execution : KelleyCompleteFirstOrderExecution n), execution.HasGapLowerBound ∧ execution.HasCallLowerBound

structure KelleyCompleteTheoremConclusion (n : ℕ) : Prop

A bundled source-facing conclusion for the complete-data Kelley theorem, with the lower-bound clause recorded under the explicit nondegenerate side condition 2 ≤ n.

• objective_value_zero : kelleyCompleteObjective 0 = 0
• origin_mem_argmin : 0 ∈ constrainedArgmin kelleyCompleteFeasibleSet kelleyCompleteObjective
• lower_bound : 2 ≤ n → KelleyCompleteLowerBoundWitness n

noncomputable def firstUnitDirection {n : ℕ} (hn : 2 ≤ n) : EuclideanSpace ℝ (Fin (n - 1))

Helper for Theorem 3.56: the first coordinate direction in ℝ^(n - 1).

theorem norm_firstUnitDirection {n : ℕ} (hn : 2 ≤ n) : ‖firstUnitDirection hn‖ = 1

Helper for Theorem 3.56: the distinguished first coordinate direction has norm 1.

theorem firstPoint_mem_kelleyCompleteFeasibleSet {n : ℕ} (hn : 2 ≤ n) : (0, firstUnitDirection hn) ∈ kelleyCompleteFeasibleSet

Helper for Theorem 3.56: the distinguished first coordinate direction lies in the explicit feasible set Q.

theorem kelleyCompleteObjective_firstPoint_eq_one {n : ℕ} (hn : 2 ≤ n) : kelleyCompleteObjective (0, firstUnitDirection hn) = 1

Helper for Theorem 3.56: the complete-data objective at the distinguished first coordinate direction is 1.

theorem kelleyComplete_gap_factor_le_one (n k : ℕ) : (1 / 4) ^ k * (√3 / 2) ^ (n - 1) ≤ 1

Helper for Theorem 3.56: the displayed geometric lower-bound factor is at most 1.

theorem exists_kelleyCompleteFirstOrderExecution_with_gap_and_call_lower_bounds {n : ℕ} (hn : 2 ≤ n) : ∃ (execution : KelleyCompleteFirstOrderExecution n), execution.HasGapLowerBound ∧ execution.HasCallLowerBound

The nondegenerate Kelley lower-bound clause for the complete-data instance.

theorem kelleyComplete_theorem_3_56 {n : ℕ} (hn : 1 ≤ n) : KelleyCompleteTheoremConclusion n

Theorem 3.56: let n ≥ 1 and consider the convex optimization problem min {f(y, x) | (y, x) ∈ Q} on ℝ × ℝ^(n - 1) with f(y, x) = max {|y|, ‖x‖²} and Q = {(y, x) | y² + ‖x‖² ≤ 1}. Then the optimal value is 0, attained at (0, 0). Moreover, the Kelley lower-bound execution is recorded here under the explicit nondegenerate side condition 2 ≤ n, which excludes the degenerate one-dimensional case n = 1.