CartanSupportPositions.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Actual Cartan positions reached by support legs

The positions are products in the nilpotent Cartan group. Their logarithms are polynomially bounded and have precisely the prescribed canonical height.

theorem OAI.PolycyclicRecognition.CartanFactorModel.exists_support_position_bound line 31

Source documentation

Each fixed support direction has an actual product position, uniformly bounded for every pivot with polynomial logarithmic coordinates.

theorem exists_support_position_bound
    (haarD : NilpotentExponentialHaarInput F.D.modelSpace F.D.carrier)
    (dynkinD : NilpotentDynkinExpansionInput F.D.modelSpace F.D.carrier)
    (π : G →* Multiplicative W)
    (hπ : ∀ x, (π (Exp x)).toAdd = eW (heightProjection T.character x))
    (w₀ : W) (w : I → W) {A : ℝ} (hA : 0 ≤ A) (p : ℕ) :
    ∃ (C : ℝ) (q : ℕ), 0 ≤ C ∧ ∀ r : ℝ, 0 ≤ r → ∀ (h₀ : H),
      ‖(finBasis ℝ H).equivFun h₀‖ ≤ A * (1 + r) ^ p →
      (π (Exp h₀)).toAdd = r • w₀ → ∀ i,
      ∃ h : H,
        Exp h = Exp h₀ * Exp (r • (supportLegDirection T H eW w₀ (w i) :
          GroupLieAlgebra (𝓘(ℝ, EG)) G)) ∧
…

Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput, OAI.PolycyclicRecognition.heightProjection, OAI.PolycyclicRecognition.supportLegDirection