RayMixedWidths.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Strictly positive mixed-word widths in a negative ray halfspace

Inside-ray supports can be negative. A sufficiently large positive outside support dominates all inside contributions in each word of the fixed bounded length. This constructs the switch template required for the ideal-fiber trajectories in boundary.tex.

theorem OAI.PolycyclicRecognition.bracketWordExponent_ge_length_lower line 24
theorem OAI.PolycyclicRecognition.bracketWordExponent_ge_mixed_lower line 35

theorem OAI.PolycyclicRecognition.exists_negative_halfspace_positive_mixed_widths line 57

Source documentation

A compact negative-height template can have strictly positive width for every mixed word in the bounded alphabet used for the cone ideal.

theorem exists_negative_halfspace_positive_mixed_widths
    {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]
    (α : V →L[ℝ] ℝ) (β : I → V →L[ℝ] ℝ)
    (v₀ : V) (hα : α v₀ < 0) (hβ : ∀ i, β i ≠ 0) (N : ℕ) :
    ∃ E : Set V, IsCompact E ∧ Convex ℝ E ∧ v₀ ∈ E ∧
      (∀ v ∈ E, α v ≤ α v₀) ∧
      ∀ w : FreeMagma I,
        IsMixedWord (fun i => (β i).toLinearMap ∉ positiveWeightRay α.toLinearMap) w →
        bracketWordLength w ≤ N →
        0 < bracketWordExponent (fun i => sSup (β i '' E)) w := by
…

Mentions: OAI.PolycyclicRecognition.IsMixedWord, OAI.PolycyclicRecognition.positiveWeightRay, OAI.PolycyclicRecognition.bracketWordLength, OAI.PolycyclicRecognition.bracketWordExponent