AffineGaussSurjectivity.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.AffineBernstein.affineEpigraph_gauss_surjective line 23

Source documentation

The full boundary above the regular base domain is covered by actual support gradients, including the direction obtained from the original graph.

theorem affineEpigraph_gauss_surjective {n : ℕ} {Ω : Set (Space n)}
    (hΩ : IsOpen Ω) (hcv : Convex ℝ Ω) {u : Space n → ℝ}
    (hu : ContDiffOn ℝ ∞ u Ω) (hp : ∀ x ∈ Ω, (hessian u x).PosDef)
    (a : Space n × ℝ) (L : (S × E) ≃L[ℝ] (Space n × ℝ))
    {B : Set S} (hB : IsOpen B)
    (hK : ∀ s ∈ B, IsCompact {y | (s,y) ∈ affineEpigraphPullback Ω u a L})
    (hzero : ∀ s ∈ B, (0:E) ∈ interior {y | (s,y) ∈ affineEpigraphPullback Ω u a L})
    {s : S} (hs : s ∈ B) {y : E} (hy : (a+L (s,y)).1 ∈ Ω)
    (hyF : affineDefining u a L (s,y) = 0) :
    let e := gradient (fun q => affineDefining u a L (s,q)) y
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.affineEpigraphPullback, OAI.AffineBernstein.affineDefining