def
ContinuousRep.orbitMap
{G : Type u_3}
[Group G]
[TopologicalSpace G]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℂ F]
(π : ContinuousRep G F)
(v : F)
:
G → F
Instances For
def
ContinuousRep.IsSmoothVector
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
(I : ModelWithCorners ℝ E H)
{G : Type u_3}
[Group G]
[TopologicalSpace G]
[ChartedSpace H G]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℂ F]
(π : ContinuousRep G F)
(v : F)
:
Instances For
def
ContinuousRep.smoothSubspace
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
(I : ModelWithCorners ℝ E H)
{G : Type u_3}
[Group G]
[TopologicalSpace G]
[ChartedSpace H G]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℂ F]
(π : ContinuousRep G F)
:
Instances For
theorem
ContinuousRep.smoothSubspace_invariant
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
(I : ModelWithCorners ℝ E H)
{G : Type u_3}
[Group G]
[TopologicalSpace G]
[ChartedSpace H G]
[LieGroup I ⊤ G]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℂ F]
(π : ContinuousRep G F)
(h : G)
(v : F)
(hv : v ∈ smoothSubspace I π)
:
noncomputable def
ContinuousRep.derivedRep
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{G : Type u_3}
[Group G]
[TopologicalSpace G]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℂ F]
(π : ContinuousRep G F)
(lieExp : E → G)
(X : E)
(v : F)
:
F