RayHalfspace.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Outside-ray weights on a negative halfspace

This is the linear-algebraic construction in the representative-independence part of boundary.tex: a nonzero form outside a positive ray is unbounded above on every fixed negative halfspace for that ray.

theorem OAI.PolycyclicRecognition.exists_large_weight_in_negative_halfspace line 26
Source documentation
A nonzero form outside the positive α ray is unbounded above while the α height stays below the height of a fixed negative point.
```
theorem exists_large_weight_in_negative_halfspace
    (α β : V →ₗ[ℝ] ℝ) (v₀ : V) (hα : α v₀ < 0)
    (hβ : β ≠ 0) (hout : β ∉ positiveWeightRay α) (R : ℝ) :
    ∃ v : V, α v ≤ α v₀ ∧ R ≤ β v := by
…
```
Mentions: OAI.PolycyclicRecognition.positiveWeightRay

theorem OAI.PolycyclicRecognition.exists_compact_negative_halfspace_template line 76

Source documentation

Finitely many outside-ray forms can simultaneously have arbitrarily large support on one compact convex set in the fixed negative halfspace.

theorem exists_compact_negative_halfspace_template
    [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul ℝ V]
    {I : Type*} [Fintype I]
    (α : V →ₗ[ℝ] ℝ) (β : I → V →ₗ[ℝ] ℝ)
    (v₀ : V) (hα : α v₀ < 0) (hβ : ∀ i, β i ≠ 0) (R : ℝ) :
    ∃ E : Set V, IsCompact E ∧ Convex ℝ E ∧ v₀ ∈ E ∧
      (∀ v ∈ E, α v ≤ α v₀) ∧
      ∀ i, β i ∉ positiveWeightRay α → ∃ v ∈ E, R ≤ β i v := by
…

Mentions: OAI.PolycyclicRecognition.positiveWeightRay