theorem family_nonempty_of_iInter_nonempty {E : Type u} {m : ℕ} {S : Fin m → Set E} (hinter : (⋂ (i : Fin m), S i).Nonempty) (i : Fin m) : (S i).Nonempty

A nonempty total intersection of a finite family gives a nonempty witness in each member of the family.

theorem lipschitzWith_convex_feasibility_max_distance {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {m : ℕ} [Nonempty (Fin m)] {S : Fin m → Set E} : LipschitzWith 1 (convex_feasibility_max_distance S)

Helper for Theorem 8.21: the max-distance objective is globally 1-Lipschitz.

noncomputable def selected_projection_direction {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {m : ℕ} {S : Fin m → Set E} (hS_closed : ∀ (i : Fin m), IsClosed (S i)) (hS_convex : ∀ (i : Fin m), Convex ℝ (S i)) (hinter : (⋂ (i : Fin m), S i).Nonempty) (z : E) (j : Fin m) : E

Helper for Theorem 8.21: the greedy step direction is the normalized residual to the selected set, with the zero branch at points already lying in that set.

theorem selected_projection_direction_mem_strongDualSubdifferential_infDist {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {m : ℕ} [Nonempty (Fin m)] {S : Fin m → Set E} (hS_closed : ∀ (i : Fin m), IsClosed (S i)) (hS_convex : ∀ (i : Fin m), Convex ℝ (S i)) (hinter : (⋂ (i : Fin m), S i).Nonempty) (z : E) (j : Fin m) : (InnerProductSpace.toDualMap ℝ E) (selected_projection_direction hS_closed hS_convex hinter z j) ∈ ∂ₛfun (y : E) => ↑(Metric.infDist y (S j))(z)

Helper for Theorem 8.21: the selected projection direction is a strong-dual subgradient of the single active distance branch.

theorem selected_farthest_direction_mem_strongDualSubdifferential_max_distance {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {m : ℕ} [Nonempty (Fin m)] {S : Fin m → Set E} (hS_closed : ∀ (i : Fin m), IsClosed (S i)) (hS_convex : ∀ (i : Fin m), Convex ℝ (S i)) (hinter : (⋂ (i : Fin m), S i).Nonempty) (z : E) (j : Fin m) (hj : ∀ (l : Fin m), Metric.infDist z (S l) ≤ Metric.infDist z (S j)) : (InnerProductSpace.toDualMap ℝ E) (selected_projection_direction hS_closed hS_convex hinter z j) ∈ ∂ₛfun (y : E) => ↑(convex_feasibility_max_distance S y)(z)

Helper for Theorem 8.21: when j is a farthest set from x, the selected projection direction is a strong-dual subgradient of the max-distance objective.

theorem norm_one_of_mem_strongDualSubdifferential_max_distance {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {m : ℕ} [Nonempty (Fin m)] {S : Fin m → Set E} {z : E} {g : StrongDual ℝ E} (hg : g ∈ ∂ₛfun (y : E) => ↑(convex_feasibility_max_distance S y)(z)) : ‖g‖ ≤ 1

Helper for Theorem 8.21: every strong-dual subgradient of the max-distance objective has norm at most 1.

theorem convex_feasibility_max_distance_subgradient_norm_bound_on_univ_norm_le {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {m : ℕ} [Nonempty (Fin m)] {S : Fin m → Set E} {z : E} {g : StrongDual ℝ E} (_hz : z ∈ Set.univ) (hg : g ∈ ∂ₛfun (y : E) => ↑(convex_feasibility_max_distance S y)(z)) : ‖g‖ ≤ 1

Helper for Theorem 8.21: the norm bound package on Set.univ uses the universal estimate ‖g‖ ≤ 1 for every strong-dual subgradient.

theorem convex_feasibility_max_distance_problem_on_univ {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {m : ℕ} [Nonempty (Fin m)] {S : Fin m → Set E} : (∀ (i : Fin m), IsClosed (S i)) → (∀ (i : Fin m), Convex ℝ (S i)) → (⋂ (j : Fin m), S j).Nonempty → IsConstrainedConvexProblem (fun (y : E) => ↑(convex_feasibility_max_distance S y)) Set.univ (⋂ (j : Fin m), S j) 0

Helper for Theorem 8.21: the max-distance convex-feasibility objective with feasible set Set.univ has optimal set ⋂ j, S j and optimal value 0.

def convex_feasibility_max_distance_subgradient_norm_bound_on_univ {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {m : ℕ} [Nonempty (Fin m)] {S : Fin m → Set E} : SubgradientNormBoundOn (fun (y : E) => ↑(convex_feasibility_max_distance S y)) Set.univ

Helper for Theorem 8.21: the max-distance objective admits the Chapter 8 norm-bound package on Set.univ with constant L_f = 1.

theorem convex_feasibility_max_distance_subgradient_norm_bound_on_univ_L_f {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {m : ℕ} [Nonempty (Fin m)] {S : Fin m → Set E} : convex_feasibility_max_distance_subgradient_norm_bound_on_univ.L_f = 1

Helper for Theorem 8.21: the packaged subgradient bound for the max-distance objective stores the source constant L_f = 1.

theorem greedy_projection_polyak_bridge {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {m : ℕ} [Nonempty (Fin m)] {S : Fin m → Set E} (hS_closed : ∀ (i : Fin m), IsClosed (S i)) (hS_convex : ∀ (i : Fin m), Convex ℝ (S i)) (hinter : (⋂ (i : Fin m), S i).Nonempty) (i : ℕ → E → Fin m) (x0 : E) (hgreedy : greedy_projection_method_is_admissible S ⋯ hS_closed hS_convex i x0) : ∃ (g : ℕ → ↑Set.univ → E) (t : ℕ → ℝ), (∀ (k : ℕ), (InnerProductSpace.toDualMap ℝ E) (g k ⟨greedy_projection_method S ⋯ hS_closed hS_convex i x0 k, ⋯⟩) ∈ ∂ₛfun (y : E) => ↑(convex_feasibility_max_distance S y)(greedy_projection_method S ⋯ hS_closed hS_convex i x0 k)) ∧ (∀ (k : ℕ), t k = polyak_stepsize (fun (y : E) => ↑(convex_feasibility_max_distance S y)) 0 (greedy_projection_method S ⋯ hS_closed hS_convex i x0 k) (g k ⟨greedy_projection_method S ⋯ hS_closed hS_convex i x0 k, ⋯⟩)) ∧ projected_subgradient_method Set.univ ⋯ ⋯ ⋯ g t ⟨x0, ⋯⟩ = fun (k : ℕ) => ⟨greedy_projection_method S ⋯ hS_closed hS_convex i x0 k, ⋯⟩

Helper for Theorem 8.21: the greedy projection trajectory can be viewed as a projected subgradient trajectory on Set.univ using a selected strong-dual subgradient of the max-distance objective and Polyak's stepsize rule.

theorem greedy_projection_method_best_max_distance_le {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {m : ℕ} [Nonempty (Fin m)] {S : Fin m → Set E} (hS_closed : ∀ (i : Fin m), IsClosed (S i)) (hS_convex : ∀ (i : Fin m), Convex ℝ (S i)) (hinter : (⋂ (i : Fin m), S i).Nonempty) (i : ℕ → E → Fin m) (x0 : E) (hgreedy : greedy_projection_method_is_admissible S ⋯ hS_closed hS_convex i x0) (k : ℕ) : best_achieved_function_value (convex_feasibility_max_distance S) (greedy_projection_method S ⋯ hS_closed hS_convex i x0) k ≤ Metric.infDist x0 (⋂ (j : Fin m), S j) / √(↑k + 1)

Theorem 8.21 (1): source part (a). For the greedy projection algorithm, the best value of the max-distance objective attained among the first k + 1 iterates is at most d_{⋂ i, S_i}(x^0) / √(k + 1).

theorem greedy_projection_method_tendsto_point_in_intersection {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {m : ℕ} [Nonempty (Fin m)] {S : Fin m → Set E} (hS_closed : ∀ (i : Fin m), IsClosed (S i)) (hS_convex : ∀ (i : Fin m), Convex ℝ (S i)) (hinter : (⋂ (i : Fin m), S i).Nonempty) (i : ℕ → E → Fin m) (x0 : E) (hgreedy : greedy_projection_method_is_admissible S ⋯ hS_closed hS_convex i x0) : ∃ xStar ∈ ⋂ (j : Fin m), S j, Filter.Tendsto (greedy_projection_method S ⋯ hS_closed hS_convex i x0) Filter.atTop (nhds xStar)

Theorem 8.21 (2): source part (b). The greedy projection sequence converges to a point in the intersection ⋂ i, S i.