StationaryConvexity.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem356.StationaryMap.stateDifferential_eq_stateDual line 22
Source documentation
The concrete scalar state differential is the product-state dual of its stationary vector field.
```
theorem stateDifferential_eq_stateDual (a y : E) (s : E × E) :
    stateDifferential a y s = stateDual E E (stationary a (y, s)) := rfl
```
Mentions: OAI.Problem356.StationaryMap.stateDifferential, OAI.Problem356.stateDual, OAI.Problem356.StationaryMap.stationary

theorem OAI.Problem356.StationaryMap.hasFDerivAt_stateStationary line 27

Source documentation

The state derivative of the concrete stationary map is the coercive regularized Coulomb Hessian.

theorem hasFDerivAt_stateStationary (a y : E) {s : E × E}
    (hxy : s.1 ≠ y) (hxz : s.1 ≠ s.2) (hzy : s.2 ≠ y) :
    HasFDerivAt (fun p : E × E => stationary a (y, p))
      (regularizedStateHessian (s.1 - y) (s.1 - s.2) (s.2 - y)) s := by
…

Mentions: OAI.Problem356.StationaryMap.stationary

theorem OAI.Problem356.StationaryMap.statePotential_strictConvexOn_of_separated line 44

Source documentation

Concrete strict convexity on every open convex state domain with the uniform pair separation used in the local construction.

theorem statePotential_strictConvexOn_of_separated (a y : E) {V : Set (E × E)}
    (hV : Convex ℝ V) (hVopen : IsOpen V)
    (hsep : ∀ s ∈ V, (2 : ℝ) / 3 ≤ ‖s.1 - y‖ ∧
      (2 : ℝ) / 3 ≤ ‖s.1 - s.2‖ ∧ (2 : ℝ) / 3 ≤ ‖s.2 - y‖) :
    StrictConvexOn ℝ V (statePotential a y) := by
…

Mentions: OAI.Problem356.StationaryMap.statePotential

theorem OAI.Problem356.StationaryMap.statePotential_minimum_and_eq_iff_of_separated line 67

Source documentation

A zero of the actual Coulomb stationary map is the unique minimizing state on a separated open convex domain.

theorem statePotential_minimum_and_eq_iff_of_separated (a y : E) {V : Set (E × E)}
    (hV : Convex ℝ V) (hVopen : IsOpen V)
    (hsep : ∀ s ∈ V, (2 : ℝ) / 3 ≤ ‖s.1 - y‖ ∧
      (2 : ℝ) / 3 ≤ ‖s.1 - s.2‖ ∧ (2 : ℝ) / 3 ≤ ‖s.2 - y‖)
    {s : E × E} (hs : s ∈ V) (hzero : stationary a (y, s) = 0)
    {q : E × E} (hq : q ∈ V) :
    statePotential a y s ≤ statePotential a y q ∧
      (statePotential a y q = statePotential a y s ↔ q = s) := by
…

Mentions: OAI.Problem356.StationaryMap.stationary, OAI.Problem356.StationaryMap.statePotential

theorem OAI.Problem356.StationaryMap.smooth_stationary_branch_support line 87

Source documentation

A smooth branch of zeros of the concrete Coulomb stationary equation produces a smooth supporting value with its exact contact graph. All analytic convexity hypotheses are discharged by the explicit distance separation.

theorem smooth_stationary_branch_support (a : E)
    {U : Set E} {V : Set (E × E)} {ψ : E → E × E} {n : WithTop ENat}
    (hV : Convex ℝ V) (hVopen : IsOpen V)
    (hsep : ∀ y ∈ U, ∀ s ∈ V, (2 : ℝ) / 3 ≤ ‖s.1 - y‖ ∧
      (2 : ℝ) / 3 ≤ ‖s.1 - s.2‖ ∧ (2 : ℝ) / 3 ≤ ‖s.2 - y‖)
    (hψ : ContDiffOn ℝ n ψ U) (hψV : MapsTo ψ U V)
    (hzero : ∀ y ∈ U, stationary a (y, ψ y) = 0) :
    ContDiffOn ℝ n (fun y => statePotential a y (ψ y)) U ∧
      ∀ y ∈ U, ∀ s ∈ V,
        statePotential a y (ψ y) ≤ statePotential a y s ∧
          (statePotential a y s = statePotential a y (ψ y) ↔ s = ψ y) := by
…

Mentions: OAI.Problem356.StationaryMap.stationary, OAI.Problem356.StationaryMap.statePotential