OAI/GroupTheory/PolycyclicRecognition/Geometry/ConeIdealFlowConjugation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The intrinsic tiling flow is ambient conjugation

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.coneIdealLetterAutomorphism_conjugation line 39

    Source documentation

    The same integrated automorphism used to partition the intrinsic ideal is conjugation by the actual ambient generator, after its inclusion in N.

    theorem coneIdealLetterAutomorphism_conjugation (i : Fin M.letterCount) (t : ℝ)
    (z : I) :
    ι (M.coneIdealLetterAutomorphism C e ExpI hExpI hbij chart hchart dynkin i t z) =
      ExpN (t • M.letter i) * ι z * (ExpN (t • M.letter i))⁻¹ := by
…
  2. theorem OAI.PolycyclicRecognition.CartanWordModel.coneIdealLetterAutomorphism_neg_apply line 52

    Source documentation

    The reverse-time flow in the anchor estimate is exactly the inverse of the automorphism in the tile covering.

    theorem coneIdealLetterAutomorphism_neg_apply (hι : Function.Injective ι)
    (i : Fin M.letterCount) (t : ℝ) (z : I) :
    M.coneIdealLetterAutomorphism C e ExpI hExpI hbij chart hchart dynkin i (-t) z =
      (M.coneIdealLetterAutomorphism C e ExpI hExpI hbij chart hchart dynkin i t).symm z := by
…