@[reducible, inline]

noncomputable abbrev uniform_simplex_point {n : ℕ} (hn : 0 < n) : ↑(WithLp.toLp 2 '' stdSimplex ℝ (Fin n))

The canonical uniform initial point x⁰ = (1 / n) e in the Euclidean simplex toLp 2 '' stdSimplex ℝ (Fin n), obtained by transporting stdSimplex.barycenter, for n > 0.

@[simp]

theorem coe_uniform_simplex_point {n : ℕ} (hn : 0 < n) : ↑(uniform_simplex_point hn) = WithLp.toLp 2 fun (x : Fin n) => 1 / ↑n

Coercing the uniform simplex point to the ambient Euclidean space gives the transported constant vector with coordinates 1 / n.

theorem bregmanDistance_halfSquaredNorm_eq_half_norm_sub_sq {n : ℕ} (x y : EuclideanSpace ℝ (Fin n)) : B[fun (z : EuclideanSpace ℝ (Fin n)) => ‖z‖ ^ 2 / 2] x y = ‖x - y‖ ^ 2 / 2

Helper for Text 9.8: for ω(x) = ‖x‖² / 2, the Bregman distance is ‖x - y‖² / 2.

theorem norm_sq_sub_le_two_of_mem_simplex {n : ℕ} {x y : EuclideanSpace ℝ (Fin n)} (hx : x ∈ WithLp.toLp 2 '' stdSimplex ℝ (Fin n)) (hy : y ∈ WithLp.toLp 2 '' stdSimplex ℝ (Fin n)) : ‖x - y‖ ^ 2 ≤ 2

Helper for Text 9.8: two transported simplex points are at squared Euclidean distance at most 2.

theorem mem_subdifferential_domain_halfSquaredNorm {n : ℕ} (z : EuclideanSpace ℝ (Fin n)) : z ∈ subdifferential_domain (Function.toEReal fun (z : EuclideanSpace ℝ (Fin n)) => ‖z‖ ^ 2 / 2)

Helper for Text 9.8: the quadratic mirror map is subdifferentiable everywhere.

instance half_squared_norm_isBregmanPotentialOn_simplex {n : ℕ} : IsBregmanPotentialOn (Function.toEReal fun (z : EuclideanSpace ℝ (Fin n)) => ‖z‖ ^ 2 / 2) (WithLp.toLp 2 '' stdSimplex ℝ (Fin n)) 1

The Euclidean mirror map ω(x) = ‖x‖² / 2 is a Bregman potential with modulus 1 on the transported simplex Δ.

theorem half_squared_norm_bregman_le_one_of_mem_simplex {n : ℕ} (hn : 0 < n) {x : EuclideanSpace ℝ (Fin n)} (hx : x ∈ WithLp.toLp 2 '' stdSimplex ℝ (Fin n)) : B[fun (z : EuclideanSpace ℝ (Fin n)) => ‖z‖ ^ 2 / 2] x ↑(uniform_simplex_point hn) ≤ 1

On the simplex, the Euclidean Bregman distance to the uniform initialization x⁰ = (1 / n)e is bounded by 1. This is the simplex specialization of the textbook constant Θ₀ = 1.

theorem euclidean_simplex_mirror_descent_best_value_gap_le {n : ℕ} {f : EuclideanSpace ℝ (Fin n) → EReal} {XStar : Set (EuclideanSpace ℝ (Fin n))} {fOpt : ℝ} (h_bound : SubgradientNormBoundOn f (WithLp.toLp 2 '' stdSimplex ℝ (Fin n))) (hn : 0 < n) {x g : ℕ → EuclideanSpace ℝ (Fin n)} {t : ℕ → ℝ} (h_problem : IsConstrainedConvexProblem f (WithLp.toLp 2 '' stdSimplex ℝ (Fin n)) XStar fOpt) (h_traj : is_mirror_descent_trajectory (fun (y : EuclideanSpace ℝ (Fin n)) => (f y).toReal) (fun (z : EuclideanSpace ℝ (Fin n)) => ‖z‖ ^ 2 / 2) (WithLp.toLp 2 '' stdSimplex ℝ (Fin n)) x g t) {xStar : EuclideanSpace ℝ (Fin n)} (hxStar : xStar ∈ XStar) (hx0 : x 0 = ↑(uniform_simplex_point hn)) {N : ℕ} (h_stepsize : ∀ (k : Fin (N + 1)), t ↑k = √2 / (h_bound.L_f * √(↑N + 1))) : best_achieved_function_value (fun (y : EuclideanSpace ℝ (Fin n)) => (f y).toReal) x N - fOpt ≤ √2 * h_bound.L_f / √(↑N + 1)

Text 9.8: for mirror descent on the Euclidean simplex with mirror map ω(x) = ‖x‖₂² / 2, uniform initialization x⁰ = (1 / n)e, and constant stepsizes t_k = √2 / (L_{f,2} √(N + 1)) on the first N + 1 iterations, the running-best objective gap is bounded by √2 L_{f,2} / √(N + 1), with L_{f,2} represented here by h_bound.L_f.

theorem projected_subgradient_method_is_mirror_descent_trajectory {n : ℕ} {f : EuclideanSpace ℝ (Fin n) → EReal} {XStar : Set (EuclideanSpace ℝ (Fin n))} {fOpt : ℝ} (g : ℕ → ↑(WithLp.toLp 2 '' stdSimplex ℝ (Fin n)) → EuclideanSpace ℝ (Fin n)) (t : ℕ → ℝ) (hn : 0 < n) (h_problem : IsConstrainedConvexProblem f (WithLp.toLp 2 '' stdSimplex ℝ (Fin n)) XStar fOpt) (h_subgrad : ∀ (k : ℕ), g k (projected_subgradient_method (WithLp.toLp 2 '' stdSimplex ℝ (Fin n)) ⋯ ⋯ ⋯ g t (uniform_simplex_point hn) k) ∈ euclideanSubdifferentialAt (fun (y : EuclideanSpace ℝ (Fin n)) => (f y).toReal) (projected_subgradient_method_iterate (WithLp.toLp 2 '' stdSimplex ℝ (Fin n)) ⋯ ⋯ ⋯ g t (uniform_simplex_point hn) k)) (h_stepsize_pos : ∀ (k : ℕ), 0 < t k) : is_mirror_descent_trajectory (fun (y : EuclideanSpace ℝ (Fin n)) => (f y).toReal) (fun (z : EuclideanSpace ℝ (Fin n)) => ‖z‖ ^ 2 / 2) (WithLp.toLp 2 '' stdSimplex ℝ (Fin n)) (projected_subgradient_method_iterate (WithLp.toLp 2 '' stdSimplex ℝ (Fin n)) ⋯ ⋯ ⋯ g t (uniform_simplex_point hn)) (fun (k : ℕ) => g k (projected_subgradient_method (WithLp.toLp 2 '' stdSimplex ℝ (Fin n)) ⋯ ⋯ ⋯ g t (uniform_simplex_point hn) k)) t

The projected-subgradient iterates on the Euclidean simplex, started at the uniform point, form the specialized mirror-descent trajectory for ω(x) = ‖x‖₂² / 2. This is the explicit Text 9.5 bridge between the Chapter 8 recursive iterates and the Chapter 9 owner is_mirror_descent_trajectory.