def DualNorm.«term‖_‖_*» : Lean.ParserDescr

def non_euclidean_gradient_method {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℝ) (counterpart : ℕ → E → E) (L : ℕ → ↑PosReal) (x0 : E) : ℕ → E

Algorithm 10.61: given an initial point x^0 = x0, a positive curvature sequence L_k, and a rule counterpart selecting a primal counterpart of the current derivative, the non-Euclidean gradient method generates iterates by x^(k+1) = x^k - (‖f'(x^k)‖_* / L_k) f'(x^k)^†.

noncomputable def non_euclidean_gradient_method_counterpart_sequence {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℝ) (counterpart : ℕ → E → E) (L : ℕ → ↑PosReal) (x0 : E) : ℕ → E

The chosen primal-counterpart sequence along the non-Euclidean gradient trajectory generated by counterpart, L, and x0.

def non_euclidean_gradient_method_is_admissible {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℝ) (counterpart : ℕ → E → E) (L : ℕ → ↑PosReal) (x0 : E) : Prop

A counterpart-selection rule is admissible for the non-Euclidean gradient method when, along the generated trajectory, each selected vector belongs to the primal-counterpart set Λ_{f'(x^k)} of the current Fréchet derivative.

@[simp]

theorem non_euclidean_gradient_method_zero {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {counterpart : ℕ → E → E} {L : ℕ → ↑PosReal} {x0 : E} : non_euclidean_gradient_method f counterpart L x0 0 = x0

The non-Euclidean gradient method starts at the prescribed initial point x^0 = x0.

theorem non_euclidean_gradient_method_succ {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {counterpart : ℕ → E → E} {L : ℕ → ↑PosReal} {x0 : E} (k : ℕ) : non_euclidean_gradient_method f counterpart L x0 (k + 1) = non_euclidean_gradient_method f counterpart L x0 k - (‖fderiv ℝ f (non_euclidean_gradient_method f counterpart L x0 k)‖ / ↑(L k)) • counterpart k (non_euclidean_gradient_method f counterpart L x0 k)

One non-Euclidean gradient step subtracts the scaled chosen primal counterpart (‖f'(x^k)‖_* / L_k) f'(x^k)^† from the current iterate.

@[simp]

theorem non_euclidean_gradient_method_counterpart_sequence_apply {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {counterpart : ℕ → E → E} {L : ℕ → ↑PosReal} {x0 : E} (k : ℕ) : non_euclidean_gradient_method_counterpart_sequence f counterpart L x0 k = counterpart k (non_euclidean_gradient_method f counterpart L x0 k)

Evaluating the counterpart sequence at k recovers the chosen primal counterpart at the kth iterate of the non-Euclidean gradient method.

theorem non_euclidean_gradient_method_differentiableAt {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {counterpart : ℕ → E → E} {L : ℕ → ↑PosReal} {x0 : E} (h : non_euclidean_gradient_method_is_admissible f counterpart L x0) (k : ℕ) : DifferentiableAt ℝ f (non_euclidean_gradient_method f counterpart L x0 k)

Under the admissibility condition, the objective is differentiable at each iterate generated by the non-Euclidean gradient method.

theorem non_euclidean_gradient_method_counterpart_mem {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {counterpart : ℕ → E → E} {L : ℕ → ↑PosReal} {x0 : E} (h : non_euclidean_gradient_method_is_admissible f counterpart L x0) (k : ℕ) : counterpart k (non_euclidean_gradient_method f counterpart L x0 k) ∈ primalCounterparts (fderiv ℝ f (non_euclidean_gradient_method f counterpart L x0 k))

Under the admissibility condition, the selected direction at iteration k belongs to the primal-counterpart set Λ_{f'(x^k)} of the current derivative.

theorem non_euclidean_gradient_method_counterpart_sequence_mem_primalCounterparts {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {counterpart : ℕ → E → E} {L : ℕ → ↑PosReal} {x0 : E} (h : non_euclidean_gradient_method_is_admissible f counterpart L x0) (k : ℕ) : non_euclidean_gradient_method_counterpart_sequence f counterpart L x0 k ∈ primalCounterparts (fderiv ℝ f (non_euclidean_gradient_method f counterpart L x0 k))

Under the admissibility condition, the chosen counterpart sequence takes values in the primal-counterpart sets of the Fréchet derivatives along the generated trajectory.