StateDual.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem356.stateDual line 19
Source documentation
The sum of the two component inner products, bundled for the usual (max-norm) product. No inner-product-space instance on the product is used.
```
def stateDual : (E × F) →L[ℝ] ((E × F) →L[ℝ] ℝ) :=
…
```
theorem OAI.Problem356.stateDual_apply line 27
theorem OAI.Problem356.stateDual_apply_comm line 31

theorem OAI.Problem356.hasFDerivAt_stateDual_comp line 36

Source documentation

Differentiating the scalar representative of a product-state gradient.

theorem hasFDerivAt_stateDual_comp {P : Type uP} [NormedAddCommGroup P]
    [NormedSpace ℝ P] {G : P → E × F} {G' : P →L[ℝ] E × F} {p : P}
    (hG : HasFDerivAt G G' p) :
    HasFDerivAt (fun q => stateDual E F (G q)) ((stateDual E F).comp G') p :=
…

Mentions: OAI.Problem356.stateDual

theorem OAI.Problem356.stateDual_comp_quadratic line 46
Source documentation
The quadratic form of the scalar Hessian agrees with the product-state coercivity expression, with the argument order used by matrix certificates.
```
theorem stateDual_comp_quadratic (A : (E × F) →L[ℝ] E × F) (v : E × F) :
    ((stateDual E F).comp A) v v =
      ⟪v.1, (A v).1⟫_ℝ + ⟪v.2, (A v).2⟫_ℝ := by
…
```
Mentions: OAI.Problem356.stateDual

theorem OAI.Problem356.strictConvexOn_of_positive_stateGradient line 54

Source documentation

A gradient with positive product-state Jacobian gives strict convexity of its scalar potential. This bridges matrix coercivity of the stationarity map to positivity of the scalar Hessian.

theorem strictConvexOn_of_positive_stateGradient
    {s : Set (E × F)} {f : E × F → ℝ} {G : E × F → E × F}
    {A : E × F → (E × F) →L[ℝ] E × F}
    (hs : Convex ℝ s) (hsopen : IsOpen s)
    (hf : ∀ z ∈ s, HasFDerivAt f (stateDual E F (G z)) z)
    (hG : ∀ z ∈ s, HasFDerivAt G (A z) z)
    (hpos : ∀ z ∈ s, ∀ v : E × F, v ≠ 0 →
      0 < ⟪v.1, (A z v).1⟫_ℝ + ⟪v.2, (A z v).2⟫_ℝ) :
    StrictConvexOn ℝ s f := by
…

Mentions: OAI.Problem356.stateDual

theorem OAI.Problem356.hasFDerivAt_zero_of_stateGradient_eq_zero line 70
Source documentation
Vanishing of the product-state gradient gives the scalar stationary condition needed by the supporting-certificate theorems.
```
theorem hasFDerivAt_zero_of_stateGradient_eq_zero
    {f : E × F → ℝ} {G : E × F → E × F} {z : E × F}
    (hf : HasFDerivAt f (stateDual E F (G z)) z) (hG : G z = 0) :
    HasFDerivAt f (0 : (E × F) →L[ℝ] ℝ) z := by
…
```
Mentions: OAI.Problem356.stateDual