OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanProfileBridgeRestriction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_profile_bridge_restrictions_of_basis line 41

   Source documentation

   The second selected path and its short bridge give one actual factor lift whose entire right cell has controlled ideal and Cartan coordinates. The exact adapted-basis identity is supplied by exists_cone_adapted_path_basis; no endpoint restriction is assumed.

   theorem exists_profile_bridge_restrictions_of_basis
       (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 →ₗ[ℝ] ℝ))
   …

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

2. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_profile_bridge_restrictions line 148

   Source documentation

   Positive ideal widths and zero quotient widths construct all of the adapted bridge data. Only the actual controlled path, its small endpoint height and the short geometric bridge remain to be supplied.

   theorem exists_profile_bridge_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 →ₗ[ℝ] ℝ))
   …

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