BoundaryRaySeparation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform separation after deleting a whole positive weight ray

The original generator list may contain repeated positive rays. A positive balanced relation still makes the remaining rays separate the height space.

theorem OAI.PolycyclicRecognition.nonpos_of_vanishing_outside_positive_ray line 21

Source documentation

A balanced positive family cannot be positive on its only nonzero ray.

theorem nonpos_of_vanishing_outside_positive_ray
    (α : I → W →ₗ[ℝ] ℝ) (c : I → ℝ) (hc : ∀ i, 0 < c i)
    (hrel : ∀ w, ∑ i, c i * α i w = 0)
    (k : I) (w : W)
    (hw : ∀ i, α i ∉ positiveWeightRay (α k) → α i w = 0) : α k w ≤ 0 := by
…

Mentions: OAI.PolycyclicRecognition.positiveWeightRay

theorem OAI.PolycyclicRecognition.separates_outside_positive_ray line 40

Source documentation

Removing every duplicate of one positive ray preserves separation.

theorem separates_outside_positive_ray
    (α : I → W →ₗ[ℝ] ℝ) (c : I → ℝ) (hc : ∀ i, 0 < c i)
    (hrel : ∀ w, ∑ i, c i * α i w = 0)
    (hsep : ∀ w, (∀ i, α i w = 0) → w = 0)
    (k : I) (w : W)
    (hw : ∀ i, α i ∉ positiveWeightRay (α k) → α i w = 0) : w = 0 := by
…

Mentions: OAI.PolycyclicRecognition.positiveWeightRay

theorem OAI.PolycyclicRecognition.exists_bound_outside_positive_ray line 61

Source documentation

The norm bound is uniform over the finite generator list, including when several generators determine the same positive ray.

theorem exists_bound_outside_positive_ray [FiniteDimensional ℝ W]
    (α : I → W →ₗ[ℝ] ℝ) (c : I → ℝ) (hc : ∀ i, 0 < c i)
    (hrel : ∀ w, ∑ i, c i * α i w = 0)
    (hsep : ∀ w, (∀ i, α i w = 0) → w = 0) :
    ∃ C : ℝ, 0 < C ∧ ∀ (k : I) (w : W) (B : ℝ), 0 ≤ B →
      (∀ i, α i ∉ positiveWeightRay (α k) → |α i w| ≤ B) → ‖w‖ ≤ C * B := by
…

Mentions: OAI.PolycyclicRecognition.positiveWeightRay