OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanFixedSamplingGeometry.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_sampling_contact_pivots line 22

   Source documentation

   Canonical-section lifts of the Euclidean contact points satisfy the root-neighbor affinity hypotheses simultaneously for all generators.

   theorem exists_sampling_contact_pivots :
       ∃ pivot : Fin M.letterCount → H, ∀ i,
         cartanHeightSection T H (heightProjection T.character (pivot i : L)) = pivot i ∧
         ‖eW (heightProjection T.character (pivot i : L))‖ = 1 ∧
         ((M.supportIn T hunimod eW).weight i).toContinuousLinearMap
           (eW (heightProjection T.character (pivot i : L))) =
             ‖((M.supportIn T hunimod eW).weight i).toContinuousLinearMap‖ ∧
         0 < M.weight i (pivot i) ∧
         eW (heightProjection T.character (pivot i : L)) ∈ M.samplingPolytope T hunimod eW ∧
         ∀ j, ((M.supportIn T hunimod eW).weight j).toContinuousLinearMap
             (eW (heightProjection T.character (pivot i : L))) =
               ‖((M.supportIn T hunimod eW).weight j).toContinuousLinearMap‖ →
   …

   Mentions: OAI.PolycyclicRecognition.cartanHeightSection, OAI.PolycyclicRecognition.heightProjection

2. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_fixed_polar_sampling_geometry line 64

   Source documentation

   All cone tests for one root use the same unit contact point. Only the positive template radius and enlargement threshold depend on the cone.

   theorem exists_fixed_polar_sampling_geometry
       (i : Fin M.letterCount) (p : W) (hp : ‖p‖ = 1)
       (hpi : ((M.supportIn T hunimod eW).weight i).toContinuousLinearMap p =
         ‖((M.supportIn T hunimod eW).weight i).toContinuousLinearMap‖)
       (K : ProperCone ℝ (StrongDual ℝ W))
       (hi : ((M.supportIn T hunimod eW).weight i).toContinuousLinearMap ∈ K)
       {c : ℝ} (hc : 0 ≤ c) :
       ∃ (ε₀ δ₀ : ℝ), 0 < ε₀ ∧ 0 < δ₀ ∧
         ∀ ε : ℝ, 0 < ε → ε ≤ ε₀ → ∀ δ : ℝ, 0 < δ → δ ≤ δ₀ →
           let w := (1 - (c + 1) * δ) • p
   …