CartanResidualBounds.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Bounds for the actual residual automorphism

We identify the residual automorphism on a nonzero root with the analytic exponential already estimated there. This removes a separate bound premise for the automorphisms constructed from the Cartan action.

theorem OAI.PolycyclicRecognition.rootInIdeal_residual_apply line 34
Source documentation
Inclusion intertwines the root residual operator and the actual ideal derivation.
```
theorem rootInIdeal_residual_apply (h : H) (v : rootSpace H χ) :
    CartanWordModel.rootInIdeal χ hχ ((rootAction H χ h - χ h • 1) v) =
      cartanIdealResidualDerivation T H h (CartanWordModel.rootInIdeal χ hχ v) := by
…
```
Mentions: OAI.PolycyclicRecognition.CartanWordModel.rootInIdeal, OAI.PolycyclicRecognition.rootAction, OAI.PolycyclicRecognition.cartanIdealResidualDerivation
theorem OAI.PolycyclicRecognition.rootInIdeal_residual_pow line 43
theorem OAI.PolycyclicRecognition.rootResidual_pow_ambient_dim line 56
Source documentation
The ambient dimension also truncates the analytic root operator.
```
theorem rootResidual_pow_ambient_dim (h : H) :
    (rootAction H χ h - χ h • 1) ^ finrank ℝ L = 0 := by
…
```
Mentions: OAI.PolycyclicRecognition.rootAction
theorem OAI.PolycyclicRecognition.rootInIdeal_residual_exp line 70
Source documentation
The polynomial Lie automorphism agrees with the analytic root residual exponential, so the earlier operator norm bounds apply to this automorphism.
```
theorem rootInIdeal_residual_exp (h : H) (v : rootSpace H χ) :
    CartanWordModel.rootInIdeal χ hχ ((NormedSpace.exp (rootAction H χ h - χ h • 1)) v) =
      cartanIdealResidualAutomorphism T H h (CartanWordModel.rootInIdeal χ hχ v) := by
…
```
Mentions: OAI.PolycyclicRecognition.CartanWordModel.rootInIdeal, OAI.PolycyclicRecognition.rootAction, OAI.PolycyclicRecognition.cartanIdealResidualAutomorphism

theorem OAI.PolycyclicRecognition.exists_residual_root_wordBasis_bound line 81

Source documentation

A common polynomial bound in every unscaled word basis.

theorem exists_residual_root_wordBasis_bound (M : CartanWordModel H) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (β : M.Bases) (h : H) (v : rootSpace H χ),
      ‖(WordBasisSelections.basis M.letter M.wordList β).equivFun
        (cartanIdealResidualAutomorphism T H h (CartanWordModel.rootInIdeal χ hχ v))‖ ≤
      C * (1 + ‖(Module.finBasis ℝ H).equivFun h‖) ^ finrank ℝ (rootSpace H χ) *
        ‖(rootCoordinates H χ) v‖ := by
…

Mentions: OAI.PolycyclicRecognition.CartanWordModel, OAI.PolycyclicRecognition.WordBasisSelections.basis, OAI.PolycyclicRecognition.cartanIdealResidualAutomorphism, OAI.PolycyclicRecognition.CartanWordModel.rootInIdeal, OAI.PolycyclicRecognition.rootCoordinates