ConeIdealGroupConjugation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Strict-width inclusions for actual group conjugation

theorem OAI.PolycyclicRecognition.CartanWordModel.coneIdealLetterFlow_exp_conjugation line 36
Source documentation
The flow in the width estimate is precisely conjugation by the corresponding generator exponential in the actual group.
```
theorem coneIdealLetterFlow_exp_conjugation (i : Fin M.letterCount)
    (t : ℝ) (v : M.coneWordIdeal C) :
    Exp (M.coneIdealLetterFlow C i t v : cartanRootIdeal H) =
      Exp (t • M.letter i) * Exp (v : cartanRootIdeal H) * (Exp (t • M.letter i))⁻¹ := by
…
```
Mentions: OAI.PolycyclicRecognition.cartanRootIdeal
theorem OAI.PolycyclicRecognition.CartanWordModel.coneIdeal_group_conjugation_absorbed line 60

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_coneIdeal_conjugation_threshold line 83

Source documentation

The enlargement threshold is derived from the positive mixed widths, independently of the time sequence and its vanishing envelope.

theorem exists_coneIdeal_conjugation_threshold
    (b₀ : Basis (Fin (finrank ℝ (M.coneWordIdeal C))) ℝ (M.coneWordIdeal C))
    (s : Fin M.letterCount → ℝ) (hs : ∀ i, 0 ≤ s i)
    (hpos : ∀ i, (M.weight i : H →ₗ[ℝ] ℝ) ∉ C → 0 < s i)
    (β : M.ConeIdealBases C) (hβ : M.IsMaximizingConeIdealBasis C b₀ s β)
    (i : Fin M.letterCount) (hi : s i = 0)
    {a b U : ℝ} (ha : 0 ≤ a) (hab : a < b) (hU : 0 < U) :
    ∃ δ₀ : ℝ, 0 < δ₀ ∧ ∀ δ : ℝ, 0 < δ → δ ≤ δ₀ →
      ∀ t ε : ℝ → ℝ, Tendsto ε atTop (𝓝 0) →
      (∀ᶠ r in atTop, |t r| ≤ Real.exp ((U * δ + ε r) * r)) →
      ∀ᶠ r in atTop,
        (fun g => Exp (t r • M.letter i) * g * (Exp (t r • M.letter i))⁻¹) ''
…