ExtremeDirectionLabels.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Constant labels on extreme horizontal directions

The generic chamber relation passes through actual approximating horizontal vectors, jointly in the base point and both times. The incident chambers then determine the extreme ray and its norm-preserving label value.

theorem OAI.PolycyclicRecognition.direction_chambers_agree_on_compact line 31
theorem OAI.PolycyclicRecognition.extreme_direction_labels_equal_on_compact line 69

theorem OAI.PolycyclicRecognition.extreme_direction_labels_equal line 97

Source documentation

Exhaustion removes the compact carrier; the exceptional set is null on the full open domain of admissible flow triples.

theorem extreme_direction_labels_equal
    (μ : Measure G) [μ.IsHaarMeasure] [μ.IsMulRightInvariant]
    (π : V →L[ℝ] W) (hπ : Function.Surjective π)
    (Exp : V → G) (hExp : Continuous Exp)
    (label : G → L) (hlabel : Measurable label)
    (A : L → W ≃ₗ[ℝ] W) (hA : ∀ l w, ‖A l w‖ = ‖w‖)
    (α : I → W →L[ℝ] ℝ) (hα : ∀ i, α i ≠ 0)
    (hsep : ∀ w : W, (∀ i, α i w = 0) → w = 0)
    (U : Set G) (hU : IsOpen U) (v : V) (σ₀ : I → Bool)
    (hσ₀ : (weightChamber α σ₀).Nonempty)
    (hExt : IsExtreme ℝ (closedWeightChamber α σ₀) (nonnegativeRay (π v)))
    (hgeneric : ∀ σ : I → Bool, incidentWeightChamber α (π v) σ →
…

Mentions: OAI.PolycyclicRecognition.weightChamber, OAI.PolycyclicRecognition.closedWeightChamber, OAI.PolycyclicRecognition.nonnegativeRay, OAI.PolycyclicRecognition.incidentWeightChamber