OAI/GroupTheory/PolycyclicRecognition/Geometry/WeightChamberLimits.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.isClosed_closedWeightChamber line 17
2. theorem OAI.PolycyclicRecognition.mem_chamber_add_smul line 23
3. theorem OAI.PolycyclicRecognition.closure_weightChamber line 30
4. theorem OAI.PolycyclicRecognition.exists_lifted_chamber_sequence line 46

   Source documentation

   The approximating horizontal vectors are explicit: add a vanishing multiple of any lift of an interior chamber vector.

   theorem exists_lifted_chamber_sequence
       {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]
       (π : V →L[ℝ] W) (hπ : Function.Surjective π)
       (α : I → W →L[ℝ] ℝ) (v : V) (σ : I → Bool)
       (hσ : incidentWeightChamber α (π v) σ) :
       ∃ u : ℕ → V, Tendsto u atTop (𝓝 v) ∧ ∀ n, π (u n) ∈ weightChamber α σ := by
   …

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

5. theorem OAI.PolycyclicRecognition.map_mem_ray_of_incident_chambers line 64

   Source documentation

   Agreement on the incident chamber images gives agreement on the ray.

   theorem map_mem_ray_of_incident_chambers
       (α : I → W →L[ℝ] ℝ) (hα : ∀ i, α i ≠ 0)
       (hsep : ∀ x : W, (∀ i, α i x = 0) → x = 0)
       {w : W} (σ₀ : I → Bool) (hσ₀ : (weightChamber α σ₀).Nonempty)
       (hExt : IsExtreme ℝ (closedWeightChamber α σ₀) (nonnegativeRay w))
       (A B : W ≃ₗ[ℝ] W)
       (himages : ∀ σ, incidentWeightChamber α w σ →
         A '' closedWeightChamber α σ = B '' closedWeightChamber α σ) :
       B w ∈ nonnegativeRay (A w) := by
   …

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

6. theorem OAI.PolycyclicRecognition.eq_on_extreme_ray_of_incident_chambers line 90

   Source documentation

   Agreement of the images of all incident closed chambers determines the value of norm-preserving labels on the extreme ray.

   theorem eq_on_extreme_ray_of_incident_chambers
       (α : I → W →L[ℝ] ℝ) (hα : ∀ i, α i ≠ 0)
       (hsep : ∀ x : W, (∀ i, α i x = 0) → x = 0)
       {w : W} (σ₀ : I → Bool) (hσ₀ : (weightChamber α σ₀).Nonempty)
       (hExt : IsExtreme ℝ (closedWeightChamber α σ₀) (nonnegativeRay w))
       (A B : W ≃ₗ[ℝ] W) (hA : ∀ x, ‖A x‖ = ‖x‖) (hB : ∀ x, ‖B x‖ = ‖x‖)
       (himages : ∀ σ, incidentWeightChamber α w σ →
         A '' closedWeightChamber α σ = B '' closedWeightChamber α σ) : A w = B w := by
   …

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

7. theorem OAI.PolycyclicRecognition.eq_on_extreme_ray_of_incident_chambers_of_gauge line 104

   Source documentation

   Any positive homogeneous gauge suffices; in particular the existing segment support norm can be used without changing normed-space instances.

   theorem eq_on_extreme_ray_of_incident_chambers_of_gauge
       (α : I → W →L[ℝ] ℝ) (hα : ∀ i, α i ≠ 0)
       (hsep : ∀ x : W, (∀ i, α i x = 0) → x = 0)
       {w : W} (σ₀ : I → Bool) (hσ₀ : (weightChamber α σ₀).Nonempty)
       (hExt : IsExtreme ℝ (closedWeightChamber α σ₀) (nonnegativeRay w))
       (p : W → ℝ) (hp : ∀ x, x ≠ 0 → 0 < p x)
       (hsmul : ∀ x r, 0 ≤ r → p (r • x) = r * p x)
       (A B : W ≃ₗ[ℝ] W) (hA : p (A w) = p w) (hB : p (B w) = p w)
       (himages : ∀ σ, incidentWeightChamber α w σ →
         A '' closedWeightChamber α σ = B '' closedWeightChamber α σ) : A w = B w := by
   …

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