structure HasQuasiNewtonLocalConvergenceAssumptions {n : ℕ} (D : Set (EuclideanSpace ℝ (Fin n))) (F : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) : Type

Chapter05 Assumption 5.4.1: F : ℝ^n → ℝ^n is continuously differentiable on an open convex set D, there is xStar ∈ D with F xStar = 0 and invertible derivative fderiv ℝ F xStar, and there is a constant gamma such that ‖fderiv ℝ F x - fderiv ℝ F xStar‖ ≤ gamma * ‖x - xStar‖ for every x ∈ D.

• open_domain : IsOpen D
• convex_domain : Convex ℝ D
• contDiffOn : ContDiffOn ℝ 1 F D
• xStar : EuclideanSpace ℝ (Fin n)
• xStar_mem : self.xStar ∈ D
• map_xStar : F self.xStar = 0
• fderiv_isInvertible : (fderiv ℝ F self.xStar).IsInvertible
• gamma : ℝ
• lipschitz_fderiv (x : EuclideanSpace ℝ (Fin n)) : x ∈ D → ‖fderiv ℝ F x - fderiv ℝ F self.xStar‖ ≤ self.gamma * ‖x - self.xStar‖

@[implicit_reducible]

instance instMembershipPointHasQuasiNewtonLocalConvergenceAssumptions {n : ℕ} {D : Set (EuclideanSpace ℝ (Fin n))} {F : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)} : Membership (EuclideanSpace ℝ (Fin n)) (HasQuasiNewtonLocalConvergenceAssumptions D F)

Membership in the local-convergence assumption package is membership in its ambient domain D.

@[simp]

theorem HasQuasiNewtonLocalConvergenceAssumptions.mem_iff {n : ℕ} {D : Set (EuclideanSpace ℝ (Fin n))} {F : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)} (h : HasQuasiNewtonLocalConvergenceAssumptions D F) (x : EuclideanSpace ℝ (Fin n)) : x ∈ h ↔ x ∈ D

@[simp]

theorem HasQuasiNewtonLocalConvergenceAssumptions.mem_xStar {n : ℕ} {D : Set (EuclideanSpace ℝ (Fin n))} {F : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)} (h : HasQuasiNewtonLocalConvergenceAssumptions D F) : h.xStar ∈ h

def HasQuasiNewtonLocalConvergenceAssumptions.xStarInDomain {n : ℕ} {D : Set (EuclideanSpace ℝ (Fin n))} {F : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)} (h : HasQuasiNewtonLocalConvergenceAssumptions D F) : ↑D

The distinguished solution xStar from Chapter05 Assumption 5.4.1 as a point of D.

noncomputable def HasQuasiNewtonLocalConvergenceAssumptions.referenceInverse {n : ℕ} {D : Set (EuclideanSpace ℝ (Fin n))} {F : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)} (h : HasQuasiNewtonLocalConvergenceAssumptions D F) : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n)

The inverse derivative F'(x*)⁻¹ attached canonically to the local-convergence assumption owner.

@[simp]

theorem HasQuasiNewtonLocalConvergenceAssumptions.coe_xStarInDomain {n : ℕ} {D : Set (EuclideanSpace ℝ (Fin n))} {F : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)} (h : HasQuasiNewtonLocalConvergenceAssumptions D F) : ↑h.xStarInDomain = h.xStar

@[simp]

theorem HasQuasiNewtonLocalConvergenceAssumptions.xStarInDomain_mem {n : ℕ} {D : Set (EuclideanSpace ℝ (Fin n))} {F : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)} (h : HasQuasiNewtonLocalConvergenceAssumptions D F) : ↑h.xStarInDomain ∈ D