ActiveRayConstraints.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The active hyperplanes of a polyhedral extreme ray

If a direction annihilates every inequality active at an extreme ray, small positive and negative perturbations stay in the cone. Extremality therefore forces that direction onto the ray's line. The cone inequalities choose the nonnegative half-line.

def OAI.PolycyclicRecognition.linearInequalityCone line 24
def OAI.PolycyclicRecognition.nonnegativeRay line 26
theorem OAI.PolycyclicRecognition.exists_two_sided_cone_perturbation line 28
theorem OAI.PolycyclicRecognition.eq_smul_of_active_constraints line 55
Source documentation
This uses the standard IsExtreme predicate on the actual nonnegative ray, rather than assuming a description of the active hyperplanes.
```
theorem eq_smul_of_active_constraints (α : I → W →L[ℝ] ℝ) {w x : W}
    (hExt : IsExtreme ℝ (linearInequalityCone α) (nonnegativeRay w))
    (hx : ∀ i, α i w = 0 → α i x = 0) : ∃ r : ℝ, x = r • w := by
…
```
Mentions: OAI.PolycyclicRecognition.linearInequalityCone, OAI.PolycyclicRecognition.nonnegativeRay
theorem OAI.PolycyclicRecognition.mem_ray_of_active_constraints line 80
theorem OAI.PolycyclicRecognition.eq_of_mem_nonnegativeRay_of_norm_eq line 100