OAI/GroupTheory/PolycyclicRecognition/Analysis/InwardFacetSegment.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_inward_facet_interval line 18

   Source documentation

   A direction pointing inward at every active constraint stays in the polyhedron for one common positive interval.

   theorem exists_inward_facet_interval
       (α : I → W →ₗ[ℝ] ℝ) (c : I → ℝ) (p v : W)
       (hp : ∀ i, α i p ≤ c i)
       (hv : ∀ i, α i p = c i → 0 ≤ α i v) :
       ∃ ε : ℝ, 0 < ε ∧ ∀ t ∈ Icc (0 : ℝ) ε, ∀ i, α i (p - t • v) ≤ c i := by
   …