OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanPivotVisits.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_segment_sampled_visit_bound line 29

   Source documentation

   Every root switch uses the prescribed segment's own supporting endpoint. Both the pivot polynomial bound and its exact height are consequences of the word chart, rather than premises of this estimate.

   theorem exists_segment_sampled_visit_bound
       (haarD : NilpotentExponentialHaarInput F.D.modelSpace F.D.carrier)
       (dynkinD : NilpotentDynkinExpansionInput F.D.modelSpace F.D.carrier)
       (hunimod : ∀ x : GroupLieAlgebra (𝓘(ℝ, EG)) G, LinearMap.trace ℝ _ (ad ℝ _ x) = 0)
       (eW : HeightSpace T.character ≃ₗ[ℝ] W) (π : G →* Multiplicative W)
       (hπ : ∀ x, (π (Exp x)).toAdd = eW (heightProjection T.character x))
       (X : I → H) (S : Finset (FreeMagma I)) (βD : WordBasisSelections X S)
       (z : Fin (finrank ℝ H) → ℝ) (v : H) {T₀ ρ : ℝ} (hT₀ : 0 ≤ T₀) (hρ : 0 ≤ ρ) :
       let P := M.supportIn T hunimod eW
   …

   Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput, OAI.PolycyclicRecognition.HeightSpace, OAI.PolycyclicRecognition.heightProjection, OAI.PolycyclicRecognition.WordBasisSelections