Polyhedron.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Finite polyhedra, local perturbations, and quotient dimension bounds.

def OAI.MatchingEntropy.finitePolyhedron line 19

theorem OAI.MatchingEntropy.finitePolyhedron_eventually_line line 23

Source documentation

Finite slack, with every active equation preserved, permits both signs.

theorem finitePolyhedron_eventually_line (L : I → (J → ℝ) →ₗ[ℝ] ℝ) (b : I → ℝ)
    {x : J → ℝ} (hx : x ∈ finitePolyhedron L b) (u : J → ℝ)
    (hu : ∀ i, L i x = b i → L i u = 0) :
    ∀ᶠ t : ℝ in 𝓝 0, x+t • u ∈ finitePolyhedron L b := by
…

Mentions: OAI.MatchingEntropy.finitePolyhedron

theorem OAI.MatchingEntropy.finitePolyhedron_eventually_expand line 42
Source documentation
Radial expansion about x preserves every active inequality for arbitrary nearby feasible points. Inactive inequalities are handled by finite slack.
```
theorem finitePolyhedron_eventually_expand (L : I → (J → ℝ) →ₗ[ℝ] ℝ) (b : I → ℝ)
    {x : J → ℝ} (hx : x ∈ finitePolyhedron L b) {t : ℝ} (ht : 0 < t) :
    ∀ᶠ y in 𝓝[finitePolyhedron L b] x, x+t⁻¹ • (y-x) ∈ finitePolyhedron L b := by
…
```
Mentions: OAI.MatchingEntropy.finitePolyhedron
theorem OAI.MatchingEntropy.extreme_point_direction_zero line 61
theorem OAI.MatchingEntropy.quotient_finrank_le_of_ker_le line 90
theorem OAI.MatchingEntropy.quotient_finrank_le_pair line 98