ConeQuotientBounds.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Polynomial residual bounds on the actual cone quotient

The nilpotent residual part of the Cartan action has polynomial coordinate growth. Passing to a quotient costs a fixed coordinate constant, obtained from lifts of a basis. These are estimates for the constructed action, with no quotient-contraction hypothesis.

theorem OAI.PolycyclicRecognition.exists_quotient_coordinate_bound line 25

Source documentation

A coordinate bound passes to an invariant quotient, with a constant depending only on the two bases and the quotient map.

theorem exists_quotient_coordinate_bound
    {V I J : Type*} [AddCommGroup V] [Module ℝ V] [Fintype I] [Fintype J]
    (a : Basis I ℝ V) (S : Submodule ℝ V) (b : Basis J ℝ (V ⧸ S)) :
    ∃ K : ℝ, 0 ≤ K ∧ ∀ (F : V →ₗ[ℝ] V) (hF : ∀ v ∈ S, F v ∈ S)
      (A : ℝ), 0 ≤ A → (∀ v, ‖a.equivFun (F v)‖ ≤ A * ‖a.equivFun v‖) →
      ∀ z, ‖b.equivFun (S.mapQ S F hF z)‖ ≤ K * A * ‖b.equivFun z‖ := by
…

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_residual_coordinate_bound line 74

Source documentation

The residual action has a polynomial bound in any fixed unscaled word basis. No unimodularity assumption is needed for this estimate.

theorem exists_residual_coordinate_bound (β : M.Bases) :
    ∃ (A : ℝ) (p : ℕ), 0 ≤ A ∧ ∀ (h : H) (v : cartanRootIdeal H),
      ‖(WordBasisSelections.basis M.letter M.wordList β).equivFun
        (cartanIdealResidualAutomorphism T H h v)‖ ≤
      A * (1 + ‖(Module.finBasis ℝ H).equivFun h‖) ^ p *
        ‖(WordBasisSelections.basis M.letter M.wordList β).equivFun v‖ := by
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.WordBasisSelections.basis, OAI.PolycyclicRecognition.cartanIdealResidualAutomorphism

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_cone_residual_coordinate_bound line 105

Source documentation

The induced residual action on every cone quotient has polynomial coordinate growth in the Cartan parameter.

theorem exists_cone_residual_coordinate_bound
    (C : Set (H →ₗ[ℝ] ℝ)) (hadd : ∀ x ∈ C, ∀ y ∈ C, x + y ∈ C)
    {J : Type*} [Fintype J]
    (b : Basis J ℝ ((cartanRootIdeal H) ⧸ M.coneWordIdeal C)) :
    ∃ (A : ℝ) (p : ℕ), 0 ≤ A ∧ ∀ (h : H) (v : (cartanRootIdeal H) ⧸ M.coneWordIdeal C),
      ‖b.equivFun ((M.coneWordIdeal C).toSubmodule.mapQ (M.coneWordIdeal C).toSubmodule
        (cartanIdealResidualAutomorphism T H h).toLinearEquiv.toLinearMap
        (M.coneWordIdeal_residual_mem T C hadd h) v)‖ ≤
      A * (1 + ‖(Module.finBasis ℝ H).equivFun h‖) ^ p * ‖b.equivFun v‖ := by
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.cartanIdealResidualAutomorphism