OAI/Analysis/AffineBernstein/ActualTubeSecond.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.homogeneousSupport_fibers_angular line 17
2. lemma OAI.AffineBernstein.homogeneousSupport_fibers_euler line 33
3. theorem OAI.AffineBernstein.affineEpigraph_tube_second_form line 46

   Source comment

   The raw affine tube has the conormal and block second form asserted in the manuscript. All differential identities have been obtained from its actual supremum support; the only geometric assumptions are the stated compact centered fibers of the original affine epigraph.

   theorem affineEpigraph_tube_second_form {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