Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.

Zero Hessian estimate constructors

Convenience constructors for second-order differentiability with zero Hessian.

theorem AleksandrovDifferentiability.hasSecondOrderExpansionAt_zero_of_affineRemainder_isLittleO {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x p : E} (h : (fun (z : E) => affineRemainder u x p (x + z)) =o[nhds 0] fun (z : E) => ‖z‖ ^ 2) : HasSecondOrderExpansionAt u x p 0

If the affine remainder is little-o of ‖z‖ ^ 2, then the second-order expansion holds with zero Hessian.

theorem AleksandrovDifferentiability.isSymmetricOperator_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : IsSymmetricOperator 0

The zero continuous linear operator is symmetric.

theorem AleksandrovDifferentiability.secondOrderDifferentiableAt_of_affineRemainder_isLittleO {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x p : E} (h : (fun (z : E) => affineRemainder u x p (x + z)) =o[nhds 0] fun (z : E) => ‖z‖ ^ 2) : SecondOrderDifferentiableAt u x

If the affine remainder is little-o of ‖z‖ ^ 2, then u is second-order differentiable at x with zero Hessian candidate.

theorem AleksandrovDifferentiability.affineRemainder_isLittleO_of_eventually_norm_le_mul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x p : E} (h : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (z : E) in nhds 0, ‖affineRemainder u x p (x + z)‖ ≤ ε * ‖z‖ ^ 2) : (fun (z : E) => affineRemainder u x p (x + z)) =o[nhds 0] fun (z : E) => ‖z‖ ^ 2

A neighborhood family of quadratic norm bounds is exactly the estimate needed to make the affine remainder little-o of ‖z‖ ^ 2. This is a Lean-friendly interface for later density and blow-up arguments, which often produce one ε-quadratic bound at a time.

theorem AleksandrovDifferentiability.hasSecondOrderExpansionAt_zero_of_eventually_norm_affineRemainder_le_mul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x p : E} (h : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (z : E) in nhds 0, ‖affineRemainder u x p (x + z)‖ ≤ ε * ‖z‖ ^ 2) : HasSecondOrderExpansionAt u x p 0

A family of local quadratic norm bounds gives a zero-Hessian second-order expansion.

theorem AleksandrovDifferentiability.secondOrderDifferentiableAt_of_eventually_norm_affineRemainder_le_mul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x p : E} (h : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (z : E) in nhds 0, ‖affineRemainder u x p (x + z)‖ ≤ ε * ‖z‖ ^ 2) : SecondOrderDifferentiableAt u x

A family of local quadratic norm bounds gives second-order differentiability with zero Hessian candidate.

theorem AleksandrovDifferentiability.affineRemainder_isLittleO_of_eventually_norm_div_norm_sq_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x p : E} (h : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (z : E) in nhdsWithin 0 {z : E | z ≠ 0}, ‖affineRemainder u x p (x + z)‖ / ‖z‖ ^ 2 ≤ ε) : (fun (z : E) => affineRemainder u x p (x + z)) =o[nhds 0] fun (z : E) => ‖z‖ ^ 2

A punctured-neighborhood normalized quotient bound is another convenient way to produce the little-o affine-remainder estimate. The value at the base point is handled separately by affineRemainder_self.

theorem AleksandrovDifferentiability.hasSecondOrderExpansionAt_zero_of_eventually_norm_div_norm_sq_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x p : E} (h : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (z : E) in nhdsWithin 0 {z : E | z ≠ 0}, ‖affineRemainder u x p (x + z)‖ / ‖z‖ ^ 2 ≤ ε) : HasSecondOrderExpansionAt u x p 0

A punctured-neighborhood normalized quotient bound gives a zero-Hessian second-order expansion.

theorem AleksandrovDifferentiability.secondOrderDifferentiableAt_of_eventually_norm_div_norm_sq_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x p : E} (h : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (z : E) in nhdsWithin 0 {z : E | z ≠ 0}, ‖affineRemainder u x p (x + z)‖ / ‖z‖ ^ 2 ≤ ε) : SecondOrderDifferentiableAt u x

A punctured-neighborhood normalized quotient bound gives second-order differentiability with zero Hessian candidate.