CartanResidualAction.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Polynomial bounds for the residual Cartan action

On an actual generalized root space, subtracting its scalar character leaves an operator nilpotent in a uniform dimension bound. Its exponential therefore has polynomial growth in the Cartan parameter. This supplies the residual operator estimate used in box conjugation.

theorem OAI.PolycyclicRecognition.exp_eq_scalar_smul_residual line 21

Source documentation

Split an arbitrary scalar character from an operator exponential.

theorem exp_eq_scalar_smul_residual
    {A : Type*} [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A]
    (a : ℝ) (X : A) :
    NormedSpace.exp X = Real.exp a • NormedSpace.exp (X - a • 1) := by
…

theorem OAI.PolycyclicRecognition.rootAction_residual_pow_eq_zero line 47
Source documentation
The nilpotence exponent is uniformly bounded by the root-space dimension.
```
theorem rootAction_residual_pow_eq_zero (h : H) :
    (rootAction H χ h - χ h • 1) ^ finrank ℝ (rootSpace H χ) = 0 := by
…
```
Mentions: OAI.PolycyclicRecognition.rootAction
def OAI.PolycyclicRecognition.rootResidualLinear line 58
Source documentation
Dependence of the residual operator on the Cartan parameter is linear.
```
def rootResidualLinear : H →ₗ[ℝ] ((rootSpace H χ) →L[ℝ] (rootSpace H χ)) where
…
```

theorem OAI.PolycyclicRecognition.exists_rootResidual_exp_bound line 72

Source documentation

One polynomial controls the residual operator for every Cartan parameter.

theorem exists_rootResidual_exp_bound :
    ∃ C : ℝ, 0 < C ∧ ∀ h : H,
      ‖NormedSpace.exp (rootAction H χ h - χ h • 1)‖ ≤
        C * (1 + ‖(Module.finBasis ℝ H).equivFun h‖) ^ finrank ℝ (rootSpace H χ) := by
…

Mentions: OAI.PolycyclicRecognition.rootAction

theorem OAI.PolycyclicRecognition.exists_rootAction_exp_bound line 101

Source documentation

Restoring the scalar character gives the full root action estimate.

theorem exists_rootAction_exp_bound :
    ∃ C : ℝ, 0 < C ∧ ∀ (h : H) (v : rootSpace H χ),
      ‖(NormedSpace.exp (rootAction H χ h)) v‖ ≤
        C * (1 + ‖(Module.finBasis ℝ H).equivFun h‖) ^ finrank ℝ (rootSpace H χ) * Real.exp (χ h) * ‖v‖ := by
…

Mentions: OAI.PolycyclicRecognition.rootAction