OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanTwoPathProbeRestrictions.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_two_path_probe_restrictions line 40

   Source documentation

   Both path estimates refer to the same target probe. The quotient region and the fixed ideal lift are constructed simultaneously, and include the entire compact right cell.

   theorem exists_two_path_probe_restrictions
       (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
       (γ₀ : M.Bases) {cell : Set (F.N.carrier × F.D.carrier)} (hcell : IsCompact cell)
       (hφ : ∀ d, F.action d = M.adjointGroupAutomorphism T F.N.equiv F.ExpN F.isExpN
         hbijN dynkinN (cartanLog H F.D.equiv F.ExpD hbijD d))
       (hpath : ∀ g : G, ∃ γ : ℝ → G, γ 0 = 1 ∧ γ 1 = g ∧
         ∀ t ∈ Icc (0 : ℝ) 1, ∀ u ∈ Icc (0 : ℝ) 1,
           dist (γ t) (γ u) ≤ dist 1 g * |t - u|)
       {Kπ : ℝ} (hKπ : 0 ≤ Kπ)
       (hLip : ∀ x y, ‖(π x).toAdd - (π y).toAdd‖ ≤ Kπ * dist x y)
       (C : Set (H →ₗ[ℝ] ℝ))
       (Q : NilpotentLieModel ((cartanRootIdeal H) ⧸ M.coneWordIdeal C))
   …

   Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.cartanLog, OAI.PolycyclicRecognition.NilpotentLieModel