SupportCoordinates.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.AffineBernstein.real_functional_surjective line 19

Source comment

A nonzero real functional has full range.

theorem real_functional_surjective (ell : E →L[ℝ] ℝ) (hne : ell ≠ 0) :
    Function.Surjective ell := by
…

theorem OAI.AffineBernstein.support_pos_of_interior line 32

Source comment

A nonzero support is strictly positive at every interior point.

theorem support_pos_of_interior {F : Set E} (ell : E →L[ℝ] ℝ) (hne : ell ≠ 0)
    (hs : ∀ y ∈ F, 0 ≤ ell y) {w : E} (hw : w ∈ interior F) : 0 < ell w := by
…

def OAI.AffineBernstein.splitFunctionalEquiv line 46
Source comment
The literal split along a normalized support vector. The second component is the kernel of the support; no quotient or degenerate coordinate is used.
```
def splitFunctionalEquiv (ell : E →L[ℝ] ℝ) (w : E) (hw : ell w = 1) :
    E ≃L[ℝ] ℝ × ell.ker :=
…
```
theorem OAI.AffineBernstein.splitFunctionalEquiv_fst line 69
theorem OAI.AffineBernstein.splitFunctionalEquiv_w line 72

theorem OAI.AffineBernstein.exists_support_coordinates line 79

Source comment

Coordinates which keep the support as the first coordinate and send a chosen interior point of a convex fiber to (1,0). Scaling the support, rather than translating the body, preserves the ambient origin and all recession rays.

theorem exists_support_coordinates {m : ℕ} {F : Set (Space m)}
    (hi : (interior F).Nonempty) (ell : Space m →L[ℝ] ℝ) (hne : ell ≠ 0)
    (hs : ∀ y ∈ F, 0 ≤ ell y) :
    ∃ (d : ℕ) (A : Space m ≃L[ℝ] ℝ × Space d),
      m = d + 1 ∧ (∀ y ∈ F, 0 ≤ (A y).1) ∧
      (1, 0) ∈ interior (A '' F) := by
…

Mentions: OAI.AffineBernstein.Space

def OAI.AffineBernstein.extendBaseEquiv line 109
Source comment
Append one real base coordinate, placing it first in Fin (k+1).
```
def extendBaseEquiv (k : ℕ) : (Space k × ℝ) ≃L[ℝ] Space (k+1) :=
…
```
Mentions: OAI.AffineBernstein.Space
def OAI.AffineBernstein.reorderThinEquiv line 115
theorem OAI.AffineBernstein.reorderThin_zero line 119
theorem OAI.AffineBernstein.reorderThin_succ line 122
theorem OAI.AffineBernstein.reorderThin_snd line 125
theorem OAI.AffineBernstein.reorderThin_sum line 128