PositiveWeightCones.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The positive parts of the ray and two-generator cones

def OAI.PolycyclicRecognition.positiveWeightRay line 16
Source documentation
The ray with its vertex omitted. Generator weights are nonzero.
```
def positiveWeightRay (α : V) : Set V := {β | ∃ c : ℝ, 0 < c ∧ β = c • α}
```
def OAI.PolycyclicRecognition.positiveWeightCone line 19
Source documentation
The pointed two-generator cone with its vertex omitted.
```
def positiveWeightCone (α η : V) : Set V :=
…
```
theorem OAI.PolycyclicRecognition.positiveWeightRay_add line 22
theorem OAI.PolycyclicRecognition.zero_not_mem_positiveWeightRay line 27
theorem OAI.PolycyclicRecognition.positiveWeightCone_add line 32
theorem OAI.PolycyclicRecognition.zero_not_mem_positiveWeightCone line 40
theorem OAI.PolycyclicRecognition.positiveWeightRay_self line 46
theorem OAI.PolycyclicRecognition.positiveWeightCone_left line 49
theorem OAI.PolycyclicRecognition.positiveWeightCone_right line 52

theorem OAI.PolycyclicRecognition.positive_sum_on_weightRay line 56

Source documentation

Positive integral multiplicities on a ray give a positive ray character.

theorem positive_sum_on_weightRay {I : Type*} [Fintype I]
    (α : V) (β : I → V) (c : I → ℕ)
    (hout : ∀ i, β i ∉ positiveWeightRay α → c i = 0)
    (i₀ : I) (h₀ : β i₀ ∈ positiveWeightRay α) (hc₀ : 0 < c i₀) :
    ∃ a : ℝ, 0 < a ∧ ∑ i, (c i : ℝ) • β i = a • α := by
…

Mentions: OAI.PolycyclicRecognition.positiveWeightRay

theorem OAI.PolycyclicRecognition.positive_sum_on_weightCone line 79

Source documentation

A two-generator cone character has a positive coefficient on each extreme ray when both corresponding generators occur.

theorem positive_sum_on_weightCone {I : Type*} [Fintype I]
    (α η : V) (hind : LinearIndependent ℝ ![α, η]) (β : I → V) (c : I → ℕ)
    (hout : ∀ i, β i ∉ positiveWeightCone α η → c i = 0)
    (i₀ i₁ : I) (h₀ : β i₀ = α) (h₁ : β i₁ = η) (hc₀ : 0 < c i₀) (hc₁ : 0 < c i₁) :
    ∃ a b : ℝ, 0 < a ∧ 0 < b ∧ ∑ i, (c i : ℝ) • β i = a • α + b • η := by
…

Mentions: OAI.PolycyclicRecognition.positiveWeightCone