OAI/GroupTheory/PolycyclicRecognition/Geometry/ConeIdealInsideAdjoint.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform ideal-box bounds for an inside adjoint

An inside letter has width zero. Adjoining it to a mixed word leaves the width unchanged, so maximizing-basis exchange bounds its adjoint uniformly in every rescaled ideal box.

  1. def OAI.PolycyclicRecognition.CartanWordModel.coneIdealLetterAdjoint line 22
  2. theorem OAI.PolycyclicRecognition.CartanWordModel.coneIdealLetterAdjoint_nilpotent line 26
  3. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_uniform_coneIdealLetterAdjoint_bound line 51

    Source documentation

    A uniform bound for the actual restricted adjoint in all maximizing ideal-box coordinates. The letter need only have zero prescribed width.

    theorem exists_uniform_coneIdealLetterAdjoint_bound
    (b₀ : Basis (Fin (finrank ℝ (M.coneWordIdeal C))) ℝ (M.coneWordIdeal C)) :
    ∃ A : ℝ, 0 ≤ A ∧ ∀ (s : Fin M.letterCount → ℝ) (β : M.ConeIdealBases C),
      M.IsMaximizingConeIdealBasis C b₀ s β →
      ∀ (i : Fin M.letterCount), s i = 0 → ∀ r : ℝ, 0 ≤ r →
      ∀ v : M.coneWordIdeal C,
      ‖(M.coneIdealBoxBasis C s β r).equivFun (M.coneIdealLetterAdjoint C i v)‖ ≤
        A * ‖(M.coneIdealBoxBasis C s β r).equivFun v‖ := by
…