OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanPolarSamplingGeometry.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_polar_sampling_geometry line 23

   Source documentation

   The contact point has positive value on the chosen root. All three translated templates lie in one open convex domain strictly inside the shrunk sampling polytope. The inward contact uses c + 1, while the concentration domain uses c.

   theorem exists_polar_sampling_geometry
       (i : Fin M.letterCount) (K : ProperCone ℝ (StrongDual ℝ W))
       (hi : ((M.supportIn T hunimod eW).weight i).toContinuousLinearMap ∈ K)
       {c : ℝ} (hc : 0 ≤ c) :
       ∃ (pivot : H) (ε₀ δ₀ : ℝ),
         cartanHeightSection T H (heightProjection T.character (pivot : L)) = pivot ∧
         0 < M.weight i pivot ∧ 0 < ε₀ ∧ 0 < δ₀ ∧
         ∀ ε : ℝ, 0 < ε → ε ≤ ε₀ → ∀ δ : ℝ, 0 < δ → δ ≤ δ₀ →
           let w := (1 - (c + 1) * δ) • eW (heightProjection T.character (pivot : L))
   …

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