structure PowellYuanAssumption1362 {n m : ℕ} (x d : ℕ → EuclideanSpace ℝ (Fin n)) (A : EuclideanSpace ℝ (Fin n) → Matrix (Fin n) (Fin m) ℝ) (B : ℕ → Matrix (Fin n) (Fin n) ℝ) : Type

Chapter13 Assumption 13.6.2: the Powell-Yuan iterates x k, trial points x k + d k, the Jacobian models A y, and the Hessian approximations B k satisfy the source assumptions that there is a bounded convex closed set omega : Set Point containing every stage iterate x k and trial point x k + d k for book indices k ≥ 1, that A y has full column rank for every y ∈ omega, and that the matrix sequence B k is uniformly bounded on book indices k ≥ 1, expressed through the equivalent finite-coordinate family fun i j ↦ (B k) i j.

• omega : Set (EuclideanSpace ℝ (Fin n))
• omega_bounded : Bornology.IsBounded self.omega
• omega_convex : Convex ℝ self.omega
• omega_closed : IsClosed self.omega
• iterate_mem_omega (k : ℕ) : 1 ≤ k → x k ∈ self.omega
• trialPoint_mem_omega (k : ℕ) : 1 ≤ k → x k + d k ∈ self.omega
• jacobian_fullColumnRank (y : EuclideanSpace ℝ (Fin n)) : y ∈ self.omega → (A y).rank = m
• matrix_bounded : Bornology.IsBounded (Set.range fun (k : ℕ) (i j : Fin n) => B (k + 1) i j)

@[implicit_reducible]

instance instMembershipPointPowellYuanAssumption1362 {n m : ℕ} {x d : ℕ → EuclideanSpace ℝ (Fin n)} {A : EuclideanSpace ℝ (Fin n) → Matrix (Fin n) (Fin m) ℝ} {B : ℕ → Matrix (Fin n) (Fin n) ℝ} : Membership (EuclideanSpace ℝ (Fin n)) (PowellYuanAssumption1362 x d A B)

Membership in PowellYuanAssumption1362 x d A B is membership in the distinguished bounded convex closed set omega from Chapter13 Assumption 13.6.2.