AffineSupport.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

def OAI.AffineBernstein.affineEpigraphFiber line 20
Source comment
A genuine affine slice of the original epigraph, in arbitrary transverse coordinates.
```
def affineEpigraphFiber {n : ℕ} (Ω : Set (Space n)) (u : Space n → ℝ)
    (x : Space n) (z : ℝ) (A : E →L[ℝ] Space n) (b : E →L[ℝ] ℝ) : Set E :=
…
```
Mentions: OAI.AffineBernstein.Space

theorem OAI.AffineBernstein.affineEpigraphFiber_no_vertical line 25

Source comment

A compact nonempty affine epigraph fiber has no vertical direction.

theorem affineEpigraphFiber_no_vertical {n : ℕ} {Ω : Set (Space n)}
    {u : Space n → ℝ} {x : Space n} {z : ℝ} {A : E →L[ℝ] Space n}
    {b : E →L[ℝ] ℝ} (hK : IsCompact (affineEpigraphFiber Ω u x z A b))
    (hne : (affineEpigraphFiber Ω u x z A b).Nonempty)
    {v : E} (hv : A v = 0) : b v = 0 := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.affineEpigraphFiber

theorem OAI.AffineBernstein.affineEpigraphFiber_injective line 55

Source comment

For an affine coordinate isomorphism compact fibers force injectivity of its horizontal linear part.

theorem affineEpigraphFiber_injective {n : ℕ} {Ω : Set (Space n)}
    {u : Space n → ℝ} {x : Space n} {z : ℝ} {A : E →L[ℝ] Space n}
    {b : E →L[ℝ] ℝ} (hK : IsCompact (affineEpigraphFiber Ω u x z A b))
    (hne : (affineEpigraphFiber Ω u x z A b).Nonempty)
    (hi : Function.Injective (fun y => (A y, b y))) : Function.Injective A := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.affineEpigraphFiber

theorem OAI.AffineBernstein.affineSlice_second line 67

Source comment

Chain rule for the actual second differential of an affine epigraph slice.

theorem affineSlice_second {n : ℕ} {u : Space n → ℝ} {x : Space n} {z : ℝ}
    {A : E →L[ℝ] Space n} {b : E →L[ℝ] ℝ} {y : E}
    (hu : ContDiffAt ℝ ∞ u (x + A y)) (v w : E) :
    fderiv ℝ (fderiv ℝ (fun q => u (x + A q) - (z + b q))) y v w =
      fderiv ℝ (fderiv ℝ u) (x + A y) (A v) (A w) := by
…

Mentions: OAI.AffineBernstein.Space

theorem OAI.AffineBernstein.sublevel_interior_strict line 92

Source comment

An interior point of a convex sublevel is a strict sublevel point whenever its actual Hessian is positive definite.

theorem sublevel_interior_strict [Nontrivial E] {W : Set E} {F : E → ℝ}
    (hcv : ConvexOn ℝ W F) {z : E}
    (hz : z ∈ interior {y | y ∈ W ∧ F y ≤ 0})
    (hd : DifferentiableAt ℝ F z)
    (hH : ∀ v : E, v ≠ 0 → 0 < fderiv ℝ (fderiv ℝ F) z v v) : F z < 0 := by
…

theorem OAI.AffineBernstein.convexOn_affineSlice line 116

Source comment

Convexity survives the actual affine slice and subtraction of its height.

theorem convexOn_affineSlice {n : ℕ} {Ω : Set (Space n)} {u : Space n → ℝ}
    (hcv : ConvexOn ℝ Ω u) (x : Space n) (z : ℝ)
    (A : E →L[ℝ] Space n) (b : E →L[ℝ] ℝ) :
    ConvexOn ℝ {y | x + A y ∈ Ω} (fun y => u (x + A y) - (z + b y)) := by
…

Mentions: OAI.AffineBernstein.Space

def OAI.AffineBernstein.affineEpigraphPullback line 137
Source comment
The literal inverse image of the original epigraph under affine coordinates.
```
def affineEpigraphPullback {n : ℕ} (Ω : Set (Space n)) (u : Space n → ℝ)
    (a : Space n × ℝ) (L : (S × E) ≃L[ℝ] (Space n × ℝ)) : Set (S × E) :=
…
```
Mentions: OAI.AffineBernstein.Space
def OAI.AffineBernstein.affineFiberHorizontal line 141
def OAI.AffineBernstein.affineFiberHeight line 145
theorem OAI.AffineBernstein.affine_coordinates_split line 149
theorem OAI.AffineBernstein.affineEpigraphPullback_fiber line 157
theorem OAI.AffineBernstein.affineFiberHorizontal_injective line 167

theorem OAI.AffineBernstein.affineEpigraph_support_smooth line 183

Source comment

The principal support-coordinate regularity assertion in tubes.tex:39–60, for actual affine images of the standing epigraph, not abstract smooth bodies. The transverse dimension is nonzero, as in the manuscript (m=n+1-k≥1).

theorem affineEpigraph_support_smooth [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 →L[ℝ] ℝ} (hℓ : ℓ ≠ 0) :
    ContDiffAt ℝ ∞ (fun q : S × (E →L[ℝ] ℝ) =>
      supportValue {y | (q.1, y) ∈ affineEpigraphPullback Ω u a L} q.2) (s, ℓ) ∧
    0 < supportValue {y | (s, y) ∈ affineEpigraphPullback Ω u a L} ℓ := by
…

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