OAI/Analysis/AffineBernstein/SupportOrientation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.supportConormal_of_level line 17
2. theorem OAI.AffineBernstein.affineEpigraph_supportConormal_inward line 50

   Source comment

   The literal support conormal is inward relative to the original solution graph, even after a general ambient affine change of variables.

   theorem affineEpigraph_supportConormal_inward [FiniteDimensional ℝ E] [Nontrivial E]
       {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) {e : E} (he : e ≠ 0) :
       let H := fun q : S × E => homogeneousSupport {y | (q.1,y) ∈ affineEpigraphPullback Ω u a L} q.2
   …

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