def HasWeightedGradientSecondOrderExpansionAt {n : ℕ} (A : { A : Matrix (Fin n) (Fin n) ℝ // A.PosDef }) (f : Matrix.PosDef.WeightedSpace A → ℝ) (g : Matrix.PosDef.WeightedSpace A) (H : Matrix.PosDef.WeightedSpace A →L[ℝ] Matrix.PosDef.WeightedSpace A) (x : Matrix.PosDef.WeightedSpace A) : Prop

The textbook weighted second-order expansion clause with linear witness g and quadratic operator witness H at x.

@[reducible, inline]

noncomputable abbrev HasWeightedGradientSecondOrderExpansionAt.total_gradient_field {A : { A : Matrix (Fin sorry) (Fin sorry) ℝ // A.PosDef }} (f : Matrix.PosDef.WeightedSpace A → ℝ) : Matrix.PosDef.WeightedSpace A → Matrix.PosDef.WeightedSpace A

Helper for Definition 1.8.4: package the totalized weighted gradient as an ordinary weighted vector field so continuity and derivative hypotheses can be specialized without reopening the gradient notation.

theorem HasWeightedGradientSecondOrderExpansionAt.total_gradient_field_continuousOn {A : { A : Matrix (Fin sorry) (Fin sorry) ℝ // A.PosDef }} {f : Matrix.PosDef.WeightedSpace A → ℝ} {x : Matrix.PosDef.WeightedSpace A} {r : ℝ} (hcont_nhds : ContinuousOn (gradient f) (Metric.ball x r)) : ContinuousOn (total_gradient_field f) (Metric.ball x r)

Helper for Definition 1.8.4: continuity of the raw weighted gradient on a neighborhood ball immediately transfers to the packaged total gradient field.

theorem HasWeightedGradientSecondOrderExpansionAt.total_gradient_field_hasFDerivAt {A : { A : Matrix (Fin sorry) (Fin sorry) ℝ // A.PosDef }} {f : Matrix.PosDef.WeightedSpace A → ℝ} {x : Matrix.PosDef.WeightedSpace A} {H : Matrix.PosDef.WeightedSpace A →L[ℝ] Matrix.PosDef.WeightedSpace A} (hgrad : HasFDerivAt (gradient f) H x) : HasFDerivAt (total_gradient_field f) H x

Helper for Definition 1.8.4: a Fréchet derivative hypothesis for the raw weighted gradient is the same derivative hypothesis for the packaged total gradient field.

theorem HasWeightedGradientSecondOrderExpansionAt.quadraticTermQuadraticBound {A : { A : Matrix (Fin sorry) (Fin sorry) ℝ // A.PosDef }} {H : Matrix.PosDef.WeightedSpace A →L[ℝ] Matrix.PosDef.WeightedSpace A} : (fun (h : Matrix.PosDef.WeightedSpace A) => 1 / 2 * Matrix.PosDef.weightedInner A (H h) h) =O[nhds 0] fun (h : Matrix.PosDef.WeightedSpace A) => Matrix.PosDef.weightedNorm A h ^ 2

Helper for Definition 1.8.4: the weighted quadratic term is uniformly bounded by a constant multiple of ‖h‖[A]^2 near the basepoint.

theorem HasWeightedGradientSecondOrderExpansionAt.quadraticTermSublinear {A : { A : Matrix (Fin sorry) (Fin sorry) ℝ // A.PosDef }} {H : Matrix.PosDef.WeightedSpace A →L[ℝ] Matrix.PosDef.WeightedSpace A} : (fun (h : Matrix.PosDef.WeightedSpace A) => 1 / 2 * Matrix.PosDef.weightedInner A (H h) h) =o[nhds 0] fun (h : Matrix.PosDef.WeightedSpace A) => h

Helper for Definition 1.8.4: the weighted quadratic term is little-o of the displacement, so it does not affect the first-order gradient witness.

theorem HasWeightedGradientSecondOrderExpansionAt.hasGradientAt_of_weighted_second_order {A : { A : Matrix (Fin sorry) (Fin sorry) ℝ // A.PosDef }} {f : Matrix.PosDef.WeightedSpace A → ℝ} {x g : Matrix.PosDef.WeightedSpace A} {H : Matrix.PosDef.WeightedSpace A →L[ℝ] Matrix.PosDef.WeightedSpace A} (hExp : HasWeightedGradientSecondOrderExpansionAt A f g H x) : sorry

Helper for Definition 1.8.4: a weighted second-order expansion already determines the weighted gradient witness.

theorem HasWeightedGradientSecondOrderExpansionAt.gradientDerivativeRemainderAtZero {A : { A : Matrix (Fin sorry) (Fin sorry) ℝ // A.PosDef }} {f : Matrix.PosDef.WeightedSpace A → ℝ} {x g : Matrix.PosDef.WeightedSpace A} {H : Matrix.PosDef.WeightedSpace A →L[ℝ] Matrix.PosDef.WeightedSpace A} (hg : sorry) (hgrad : HasFDerivAt (gradient f) H x) : (fun (k : Matrix.PosDef.WeightedSpace A) => gradient f (x + k) - g - H k) =o[nhds 0] fun (k : Matrix.PosDef.WeightedSpace A) => k

Helper for Definition 1.8.4: translating the derivative of the weighted totalized gradient to the basepoint gives the vector little-o remainder in displacement coordinates.

theorem HasWeightedGradientSecondOrderExpansionAt.segment_point_mem_ball {A : { A : Matrix (Fin sorry) (Fin sorry) ℝ // A.PosDef }} {x : Matrix.PosDef.WeightedSpace A} {r : ℝ} (hr : 0 < r) {h : Matrix.PosDef.WeightedSpace A} (hh : ‖h‖ < r) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : x + t • h ∈ Metric.ball x r

Helper for Definition 1.8.4: every point on a short weighted segment from x stays inside the radius-r ball where the local gradient-field hypothesis is available.

theorem HasWeightedGradientSecondOrderExpansionAt.segment_quadratic_remainder_hasDerivAt {A : { A : Matrix (Fin sorry) (Fin sorry) ℝ // A.PosDef }} {f : Matrix.PosDef.WeightedSpace A → ℝ} {x g : Matrix.PosDef.WeightedSpace A} {H : Matrix.PosDef.WeightedSpace A →L[ℝ] Matrix.PosDef.WeightedSpace A} {r : ℝ} (hr : 0 < r) (hgrad_nhds : ∀ y ∈ Metric.ball x r, sorry) {h : Matrix.PosDef.WeightedSpace A} (hh : ‖h‖ < r) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : HasDerivAt (fun (u : ℝ) => f (x + u • h) - f x - u * Matrix.PosDef.weightedInner A g h - 1 / 2 * u ^ 2 * Matrix.PosDef.weightedInner A (H h) h) (Matrix.PosDef.weightedInner A (gradient f (x + t • h) - g - t • H h) h) t

Helper for Definition 1.8.4: along a short weighted segment, the corrected quadratic remainder has derivative equal to the gradient linearization error paired with the segment direction.

theorem HasWeightedGradientSecondOrderExpansionAt.weighted_segment_pair_continuousOn {A : { A : Matrix (Fin sorry) (Fin sorry) ℝ // A.PosDef }} {s : Set ℝ} {v : ℝ → Matrix.PosDef.WeightedSpace A} (hv : ContinuousOn v s) (h : Matrix.PosDef.WeightedSpace A) : ContinuousOn (fun (t : ℝ) => Matrix.PosDef.weightedInner A (v t) h) s

Helper for Definition 1.8.4: pairing a continuous weighted vector field with a fixed weighted direction preserves continuity on the same set.

theorem HasWeightedGradientSecondOrderExpansionAt.segment_affine_map_continuousOn {A : { A : Matrix (Fin sorry) (Fin sorry) ℝ // A.PosDef }} {x : Matrix.PosDef.WeightedSpace A} (h : Matrix.PosDef.WeightedSpace A) : ContinuousOn (fun (t : ℝ) => x + t • h) (Set.Icc 0 1)

Helper for Definition 1.8.4: the affine segment map t ↦ x + t • h is continuous on [0,1].

theorem HasWeightedGradientSecondOrderExpansionAt.segment_affine_model_continuousOn {A : { A : Matrix (Fin sorry) (Fin sorry) ℝ // A.PosDef }} {g : Matrix.PosDef.WeightedSpace A} {H : Matrix.PosDef.WeightedSpace A →L[ℝ] Matrix.PosDef.WeightedSpace A} (h : Matrix.PosDef.WeightedSpace A) : ContinuousOn (fun (t : ℝ) => g + t • H h) (Set.Icc 0 1)

Helper for Definition 1.8.4: the affine gradient/Hessian model t ↦ g + t • H h is continuous on [0,1].

theorem HasWeightedGradientSecondOrderExpansionAt.segment_model_continuousOn_of_vector_field {A : { A : Matrix (Fin sorry) (Fin sorry) ℝ // A.PosDef }} {x g : Matrix.PosDef.WeightedSpace A} {H : Matrix.PosDef.WeightedSpace A →L[ℝ] Matrix.PosDef.WeightedSpace A} {G : Matrix.PosDef.WeightedSpace A → Matrix.PosDef.WeightedSpace A} {r : ℝ} (hr : 0 < r) (hcont_nhds : ContinuousOn G (Metric.ball x r)) {h : Matrix.PosDef.WeightedSpace A} (hh : ‖h‖ < r) : ContinuousOn (fun (t : ℝ) => G (x + t • h) - g - t • H h) (Set.Icc 0 1)

Helper for Definition 1.8.4: a continuous local weighted vector field stays continuous after pullback to a short segment and subtraction of the affine model.

theorem HasWeightedGradientSecondOrderExpansionAt.segment_vector_field_continuousAt {A : { A : Matrix (Fin sorry) (Fin sorry) ℝ // A.PosDef }} {x : Matrix.PosDef.WeightedSpace A} {G : Matrix.PosDef.WeightedSpace A → Matrix.PosDef.WeightedSpace A} {r : ℝ} (hr : 0 < r) (hcont_nhds : ContinuousOn G (Metric.ball x r)) {h : Matrix.PosDef.WeightedSpace A} (hh : ‖h‖ < r) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : ContinuousAt (fun (s : ℝ) => G (x + s • h)) t

Helper for Definition 1.8.4: if the weighted gradient is continuous on a neighborhood ball of x, then its pullback along a short affine segment is continuous at each parameter value in [0,1].

theorem HasWeightedGradientSecondOrderExpansionAt.segment_raw_gradient_continuousAt {A : { A : Matrix (Fin sorry) (Fin sorry) ℝ // A.PosDef }} {f : Matrix.PosDef.WeightedSpace A → ℝ} {x : Matrix.PosDef.WeightedSpace A} {r : ℝ} (hr : 0 < r) (hcont_nhds : ContinuousOn (gradient f) (Metric.ball x r)) {h : Matrix.PosDef.WeightedSpace A} (hh : ‖h‖ < r) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : ContinuousAt (fun (s : ℝ) => gradient f (x + s • h)) t

Helper for Definition 1.8.4: if the weighted gradient is continuous on a neighborhood ball of x, then its pullback along a short affine segment is continuous at each parameter value in [0,1].

theorem HasWeightedGradientSecondOrderExpansionAt.segment_gradient_model_continuousOn {A : { A : Matrix (Fin sorry) (Fin sorry) ℝ // A.PosDef }} {f : Matrix.PosDef.WeightedSpace A → ℝ} {x g : Matrix.PosDef.WeightedSpace A} {H : Matrix.PosDef.WeightedSpace A →L[ℝ] Matrix.PosDef.WeightedSpace A} {r : ℝ} (hr : 0 < r) (hcont_nhds : ContinuousOn (gradient f) (Metric.ball x r)) {h : Matrix.PosDef.WeightedSpace A} (hh : ‖h‖ < r) : ContinuousOn (fun (t : ℝ) => gradient f (x + t • h) - g - t • H h) (Set.Icc 0 1)

Helper for Definition 1.8.4: the affine-segment gradient error field is continuous on [0,1] once the gradient is continuous on a neighborhood ball of x.

theorem HasWeightedGradientSecondOrderExpansionAt.segment_quadratic_integrand_continuous {A : { A : Matrix (Fin sorry) (Fin sorry) ℝ // A.PosDef }} {f : Matrix.PosDef.WeightedSpace A → ℝ} {x g : Matrix.PosDef.WeightedSpace A} {H : Matrix.PosDef.WeightedSpace A →L[ℝ] Matrix.PosDef.WeightedSpace A} {r : ℝ} (hr : 0 < r) (hcont_nhds : ContinuousOn (gradient f) (Metric.ball x r)) {h : Matrix.PosDef.WeightedSpace A} (hh : ‖h‖ < r) : ContinuousOn (fun (t : ℝ) => Matrix.PosDef.weightedInner A (gradient f (x + t • h) - g - t • H h) h) (Set.Icc 0 1)

Helper for Definition 1.8.4: along a short weighted segment, the gradient linearization error paired with the segment direction is continuous on [0,1].

theorem HasWeightedGradientSecondOrderExpansionAt.norm_smul_le_of_mem_Icc {A : { A : Matrix (Fin sorry) (Fin sorry) ℝ // A.PosDef }} {h : Matrix.PosDef.WeightedSpace A} {t : ℝ} (ht : t ∈ Set.Icc 0 1) : ‖t • h‖ ≤ ‖h‖

Helper for Definition 1.8.4: segment scaling by a parameter in [0,1] does not increase the weighted norm.

theorem HasWeightedGradientSecondOrderExpansionAt.smul_mem_ball_zero_of_mem_Icc {A : { A : Matrix (Fin sorry) (Fin sorry) ℝ // A.PosDef }} {δ : ℝ} {h : Matrix.PosDef.WeightedSpace A} (hh : h ∈ Metric.ball 0 δ) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : t • h ∈ Metric.ball 0 δ

Helper for Definition 1.8.4: if a displacement lies in a ball around the origin, then every scaled segment point t • h with t ∈ [0,1] stays in the same ball.

theorem HasWeightedGradientSecondOrderExpansionAt.scaledSegmentDerivativeRemainderBound {A : { A : Matrix (Fin sorry) (Fin sorry) ℝ // A.PosDef }} {f : Matrix.PosDef.WeightedSpace A → ℝ} {x g : Matrix.PosDef.WeightedSpace A} {H : Matrix.PosDef.WeightedSpace A →L[ℝ] Matrix.PosDef.WeightedSpace A} (hg : sorry) (hgrad : HasFDerivAt (gradient f) H x) (ε : ℝ) : ε > 0 → ∀ᶠ (h : Matrix.PosDef.WeightedSpace A) in nhds 0, ∀ t ∈ Set.Icc 0 1, ‖gradient f (x + t • h) - g - H (t • h)‖ ≤ ε * ‖t • h‖

Helper for Definition 1.8.4: the derivative remainder of the weighted totalized gradient is uniformly controlled along scaled segments once the displacement is sufficiently small.

theorem HasWeightedGradientSecondOrderExpansionAt.gradient_linearization_on_segment_abs_le {A : { A : Matrix (Fin sorry) (Fin sorry) ℝ // A.PosDef }} {f : Matrix.PosDef.WeightedSpace A → ℝ} {x g : Matrix.PosDef.WeightedSpace A} {H : Matrix.PosDef.WeightedSpace A →L[ℝ] Matrix.PosDef.WeightedSpace A} (hg : sorry) (hgrad : HasFDerivAt (gradient f) H x) (ε : ℝ) : ε > 0 → ∀ᶠ (h : Matrix.PosDef.WeightedSpace A) in nhds 0, ∀ t ∈ Set.Icc 0 1, |Matrix.PosDef.weightedInner A (gradient f (x + t • h) - g - t • H h) h| ≤ ε * t * ‖h‖ ^ 2

Helper for Definition 1.8.4: the Fréchet derivative of the weighted totalized gradient gives a uniform ε * t * ‖h‖² bound for the segment integrand once h is small.

theorem HasWeightedGradientSecondOrderExpansionAt.lineNormSquareQuadraticBound {A : { A : Matrix (Fin sorry) (Fin sorry) ℝ // A.PosDef }} (d : Matrix.PosDef.WeightedSpace A) : (fun (t : ℝ) => Matrix.PosDef.weightedNorm A (t • d) ^ 2) =O[nhds 0] fun (t : ℝ) => t ^ 2

Helper for Definition 1.8.4: along a fixed weighted line, the quadratic norm ‖t • d‖[A]^2 is bounded by a constant multiple of t^2.

theorem HasWeightedGradientSecondOrderExpansionAt.line_model_apply {A : { A : Matrix (Fin sorry) (Fin sorry) ℝ // A.PosDef }} {f : Matrix.PosDef.WeightedSpace A → ℝ} {x g : Matrix.PosDef.WeightedSpace A} {H : Matrix.PosDef.WeightedSpace A →L[ℝ] Matrix.PosDef.WeightedSpace A} (d : Matrix.PosDef.WeightedSpace A) (t : ℝ) : f (x + t • d) - (f x + t * Matrix.PosDef.weightedInner A g d + 1 / 2 * t ^ 2 * Matrix.PosDef.weightedInner A (H d) d) = (fun (h : Matrix.PosDef.WeightedSpace A) => f (x + h) - (f x + Matrix.PosDef.weightedInner A g h + 1 / 2 * Matrix.PosDef.weightedInner A (H h) h)) (t • d)

Helper for Definition 1.8.4: evaluating the weighted quadratic model on a line rewrites the source remainder into the scalar line-restriction form.

theorem HasWeightedGradientSecondOrderExpansionAt.line_restriction_has_weighted_second_order_expansion {A : { A : Matrix (Fin sorry) (Fin sorry) ℝ // A.PosDef }} {f : Matrix.PosDef.WeightedSpace A → ℝ} {x g : Matrix.PosDef.WeightedSpace A} {H : Matrix.PosDef.WeightedSpace A →L[ℝ] Matrix.PosDef.WeightedSpace A} (hExp : HasWeightedGradientSecondOrderExpansionAt A f g H x) (d : Matrix.PosDef.WeightedSpace A) : (fun (t : ℝ) => f (x + t • d) - (f x + t * Matrix.PosDef.weightedInner A g d + 1 / 2 * t ^ 2 * Matrix.PosDef.weightedInner A (H d) d)) =o[nhds 0] fun (t : ℝ) => t ^ 2

Helper for Definition 1.8.4: restricting the weighted quadratic expansion to a fixed line records the textbook quadratic coefficient ⟪H d, d⟫_[A].