CartanGoodCellLegs.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Good physical legs on the actual translated Cartan Haar cells

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_good_cartan_cell_legs_sequence line 33

Source documentation

A supported coordinate profile supplies actual good group sheets. Their relative Haar mass, their positivity and every physical segment leg are proved together, with the original translated cell retained.

theorem exists_good_cartan_cell_legs_sequence
    (haarN : NilpotentExponentialHaarInput F.N.modelSpace F.N.carrier)
    (chartN : GroupLieAlgebra (𝓘(ℝ, F.N.modelSpace)) F.N.carrier ≃ₜ F.N.carrier)
    (hchartN : ∀ x, chartN x = F.ExpN x)
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    (E : Set W) (β : M.Bases)
    (scale : ℕ → ℝ) (hscale : Tendsto scale atTop atTop) (k : ℕ → cartanRootIdeal H)
    (X : I → H) {d : ℕ} (hDnil : lowerCentralSeries ℝ H H d = ⊥)
    (bD₀ : Basis (Fin (finrank ℝ H)) ℝ H)
    (βD : WordBasisSelections X (boundedBracketWords d))
    (hβD : IsMaximizingColumnBasis (wordListCoordinates X (boundedBracketWords d) bD₀)
      (fun w => bracketWordExponent (fun _ : I => 1) w) βD.val)
…

Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.boundedBracketWords, OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.bracketWordExponent