CartanProfilePivot.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A total profile base point at the moving physical pivot

theorem OAI.PolycyclicRecognition.CartanFactorModel.exists_profile_pivot line 25

Source documentation

Only the finite initial segment uses a fallback. Eventually the total subtype-valued base point is the exact physical pivot, with its unchanged height. No extra base point membership hypothesis is needed for small scales.

theorem CartanFactorModel.exists_profile_pivot
    (X : I → H) (S : Finset (FreeMagma I)) (β : WordBasisSelections X S)
    (h : H →ₗ[ℝ] W) (hh : ∀ x y : H, h ⁅x, y⁆ = 0)
    (scale : ℕ → ℝ) (hs0 : ∀ n, 0 < scale n) (pivot : H)
    (Z : Set (Fin (finrank ℝ H) → ℝ))
    (hp : ∀ᶠ n in atTop,
      (exponentialRescaleBasis (WordBasisSelections.basis X S β)
        (fun j => bracketWordExponent (fun _ : I => 1) (β.val j))
        (Real.log (scale n))).equivFun (scale n • pivot) ∈ Z) :
    let b := WordBasisSelections.basis X S β
…

Mentions: OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.exponentialRescaleBasis, OAI.PolycyclicRecognition.WordBasisSelections.basis, OAI.PolycyclicRecognition.bracketWordExponent