StrictMinimum.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem356.convex_isMinOn_of_hasFDerivAt_zero line 18

Source documentation

A stationary point of a convex differentiable function is a global minimizer on its convexity domain.

theorem convex_isMinOn_of_hasFDerivAt_zero {s : Set E} {f : E → ℝ} {x : E}
    (hf : ConvexOn ℝ s f) (hx : x ∈ s)
    (hd : HasFDerivAt f (0 : E →L[ℝ] ℝ) x) : IsMinOn f s x := by
…

theorem OAI.Problem356.strictConvex_eq_iff_of_hasFDerivAt_zero line 34

Source documentation

Strict convexity upgrades a stationary point to the unique minimum.

theorem strictConvex_eq_iff_of_hasFDerivAt_zero {s : Set E} {f : E → ℝ} {x : E}
    (hf : StrictConvexOn ℝ s f) (hx : x ∈ s)
    (hd : HasFDerivAt f (0 : E →L[ℝ] ℝ) x) {y : E} (hy : y ∈ s) :
    f y = f x ↔ y = x := by
…

theorem OAI.Problem356.strictConvexOn_of_line_deriv2_pos line 52

Source documentation

Strict positivity of second derivatives on nonconstant line segments implies strict convexity in an arbitrary real normed space.

theorem strictConvexOn_of_line_deriv2_pos {s : Set E} {f : E → ℝ}
    (hs : Convex ℝ s) (hf : ContinuousOn f s)
    (hpos : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → ∀ t ∈ Ioo (0 : ℝ) 1,
      0 < deriv (deriv (f ∘ AffineMap.lineMap x y)) t) :
    StrictConvexOn ℝ s f := by
…

theorem OAI.Problem356.strictConvexOn_of_positive_hessian line 79

Source documentation

A positive-definite second Fréchet derivative gives strict convexity on an open convex domain. The two derivative fields are explicit, so this applies directly to computed Hessians without rewriting fderiv.

theorem strictConvexOn_of_positive_hessian {s : Set E} {f : E → ℝ}
    {f' : E → E →L[ℝ] ℝ} {f'' : E → E →L[ℝ] E →L[ℝ] ℝ}
    (hs : Convex ℝ s) (hsopen : IsOpen s)
    (hf : ∀ z ∈ s, HasFDerivAt f (f' z) z)
    (hf' : ∀ z ∈ s, HasFDerivAt f' (f'' z) z)
    (hpos : ∀ z ∈ s, ∀ v : E, v ≠ 0 → 0 < f'' z v v) :
    StrictConvexOn ℝ s f := by
…

theorem OAI.Problem356.stationary_family_certificate line 109

Source documentation

A smooth stationary branch in strictly convex state slices defines a smooth supporting value, and its graph is exactly the contact set.

theorem stationary_family_certificate
    {P : Type uP} [NormedAddCommGroup P] [NormedSpace ℝ P]
    {U : Set P} {V : Set E} {n : WithTop ENat}
    {F : P × E → ℝ} {ψ : P → E}
    (hF : ContDiffOn ℝ n F (U ×ˢ V)) (hψ : ContDiffOn ℝ n ψ U)
    (hψV : MapsTo ψ U V)
    (hconv : ∀ p ∈ U, StrictConvexOn ℝ V (fun z => F (p, z)))
    (hstat : ∀ p ∈ U, HasFDerivAt (fun z => F (p, z))
      (0 : E →L[ℝ] ℝ) (ψ p)) :
    ContDiffOn ℝ n (fun p => F (p, ψ p)) U ∧
      ∀ p ∈ U, ∀ z ∈ V,
        F (p, ψ p) ≤ F (p, z) ∧ (F (p, z) = F (p, ψ p) ↔ z = ψ p) := by
…

theorem OAI.Problem356.stationary_family_certificate_of_positive_hessian line 130

Source documentation

Version of stationary_family_certificate using explicit positive Hessians. This is the analytic supporting-certificate step of the local construction.

theorem stationary_family_certificate_of_positive_hessian
    {P : Type uP} [NormedAddCommGroup P] [NormedSpace ℝ P]
    {U : Set P} {V : Set E} {n : WithTop ENat}
    {F : P × E → ℝ} {ψ : P → E}
    {D : P → E → E →L[ℝ] ℝ} {H : P → E → E →L[ℝ] E →L[ℝ] ℝ}
    (hF : ContDiffOn ℝ n F (U ×ˢ V)) (hψ : ContDiffOn ℝ n ψ U)
    (hψV : MapsTo ψ U V) (hV : Convex ℝ V) (hVopen : IsOpen V)
    (hD : ∀ p ∈ U, ∀ z ∈ V, HasFDerivAt (fun z => F (p, z)) (D p z) z)
    (hH : ∀ p ∈ U, ∀ z ∈ V, HasFDerivAt (D p) (H p z) z)
    (hpos : ∀ p ∈ U, ∀ z ∈ V, ∀ v : E, v ≠ 0 → 0 < H p z v v)
    (hstat : ∀ p ∈ U, D p (ψ p) = 0) :
    ContDiffOn ℝ n (fun p => F (p, ψ p)) U ∧
…