OAI/GroupTheory/PolycyclicRecognition/Geometry/ActualSmoothRotation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The smooth rotational modification from the actual Cartan factors

The chosen compact action retains its factor formula. This constructs a smooth graph group; its Lie algebra identification and triangular matrix realization are separate steps.

  1. def OAI.PolycyclicRecognition.ComplexWeightFactorModel.factorCompactRotationAction line 27
  2. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.factorCompactRotationAction_formula line 31
  3. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.continuous_factorCompactRotationAction line 38
  4. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.factorCompactRotationAction_invariant line 43
  5. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.contMDiff_inverse_factorCompactRotationAction line 48
  6. abbrev OAI.PolycyclicRecognition.ComplexWeightFactorModel.SmoothRotationalModification line 56
  7. def OAI.PolycyclicRecognition.ComplexWeightFactorModel.smoothRotationalModificationChartedSpace line 61
  8. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.smoothRotationalModificationLieGroup line 69

    Source documentation

    Both operations of the actual graph group are infinitely differentiable.

    theorem smoothRotationalModificationLieGroup : LieGroup (𝓘(ℝ,E)) ∞ (F.SmoothRotationalModification hExp) := by
…
  9. def OAI.PolycyclicRecognition.ComplexWeightFactorModel.smoothRotationalModificationHomeomorph line 75