OAI/GroupTheory/PolycyclicRecognition/Algebra/RealTorusContinuity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Continuity of the real compact rotation action

  1. theorem OAI.PolycyclicRecognition.realTorusOperator_fixes_cartan line 16
  2. def OAI.PolycyclicRecognition.realPhaseHom line 24

    Source documentation

    Additive Cartan parameters act through the compact rotation group.

    def realPhaseHom : Multiplicative H →* realRotationTorus L H where
…

    Mentions: OAI.PolycyclicRecognition.realRotationTorus

  3. theorem OAI.PolycyclicRecognition.continuous_realTorusOperator line 63

    Source documentation

    The compact real torus acts jointly continuously on the real algebra.

    theorem continuous_realTorusOperator :
    Continuous (fun p : realRotationTorus L H × L => realTorusOperator L H p.1 p.2) := by
…

    Mentions: OAI.PolycyclicRecognition.realRotationTorus, OAI.PolycyclicRecognition.realTorusOperator

  4. theorem OAI.PolycyclicRecognition.continuous_realPhaseVector line 79

    Source documentation

    Cartan rotations depend continuously on the real Cartan parameter.

    theorem continuous_realPhaseVector : Continuous (realPhaseVector L H) := by
…

    Mentions: OAI.PolycyclicRecognition.realPhaseVector