CartanProfileEndpointLifts.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Common factor boxes for families of controlled paths

Vanishing height errors are absorbed in one fixed maximizing basis. The endpoint and its compact right thickening share the same chosen factor lift.

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_sequence_profile_endpoint_lifts line 41

Source documentation

An unthickened endpoint lift retains the exact endpoint height and its common subexponential boxes. This choice is made before the short bridge.

theorem exists_sequence_profile_endpoint_lifts
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    (γ₀ : M.Bases)
    (hφ : ∀ d, F.action d = M.adjointGroupAutomorphism T F.N.equiv F.ExpN F.isExpN
      (by rw [← show chartN = F.ExpN from funext hchartN]; exact chartN.bijective) dynkinN
      (cartanLog H F.D.equiv F.ExpD
        (by rw [← show chartD = F.ExpD from funext hchartD]; exact chartD.bijective) 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)
…

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