AffinePolytope.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem326.Affine.labelPolytope line 10
Source documentation
The superlevel set of every member of a finite affine family.
```
def labelPolytope {d : ℕ} (Λ : Finset (Label d)) (h M : ℝ) :
    Set (Fin d → ℝ) := {x | ∀ L ∈ Λ, M ≤ L.value h x}
```
Mentions: OAI.Problem326.Affine.Label
lemma OAI.Problem326.Affine.labelPolytope_isFinitePolyhedron line 13
lemma OAI.Problem326.Affine.labelPolytope_active_iff line 22

lemma OAI.Problem326.Affine.exists_compact_labelPolytope line 37

Source documentation

The geometric part of the affine trapping construction, with the canonical label and activity definitions. Only the activity certificates are assumed; no differential equation or global-solution assertion is used.

lemma exists_compact_labelPolytope {d : ℕ}
    (Λ : Finset (Label d)) (hne : Λ.Nonempty) (h : ℝ)
    (B : Set (Fin d → ℝ)) (x0 : Fin d → ℝ)
    (hB : IsCompact B) (hx0B : x0 ∈ interior B)
    (hinitial : ∀ L, Active Λ L h x0 → L.slope = 0)
    (hboundary : ∀ x ∈ frontier B, ∀ L, Active Λ L h x → L.slope ≠ 0) :
    ∃ L0, Active Λ L0 h x0 ∧ L0.slope = 0 ∧
      IsCompact (labelPolytope Λ h (L0.offset h)) ∧
      Convex ℝ (labelPolytope Λ h (L0.offset h)) ∧
      IsFinitePolyhedron (labelPolytope Λ h (L0.offset h)) ∧
      x0 ∈ labelPolytope Λ h (L0.offset h) ∧
      labelPolytope Λ h (L0.offset h) ⊆ interior B := by
…

Mentions: OAI.Problem326.Affine.Label, OAI.Problem326.Affine.Active, OAI.Problem326.Affine.labelPolytope, OAI.Problem326.IsFinitePolyhedron