structure ContinuousRepresentation (G : Type u_1) [Group G] [TopologicalSpace G] (V : Type u_2) [AddCommGroup V] [Module ℂ V] [TopologicalSpace V] : Type (max u_1 u_2)

• toMonoidHom : G →* V →L[ℂ] V
• continuous_action : Continuous fun (p : G × V) => (self.toMonoidHom p.1) p.2

def ContinuousRepresentation.orbitMap {G : Type u_1} [Group G] [TopologicalSpace G] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRepresentation G F) (v : F) : G → F

def ContinuousRepresentation.IsSmoothVector {G : Type u_1} [Group G] [TopologicalSpace G] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) [ChartedSpace H G] (π : ContinuousRepresentation G F) (v : F) : Prop

def ContinuousRepresentation.smoothVectors {G : Type u_1} [Group G] [TopologicalSpace G] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) [ChartedSpace H G] (π : ContinuousRepresentation G F) : Set F

def ContinuousRepresentation.IsGFiniteVector {G : Type u_1} [Group G] [TopologicalSpace G] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRepresentation G F) (v : F) : Prop

def ContinuousRepresentation.gFiniteVectors {G : Type u_1} [Group G] [TopologicalSpace G] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRepresentation G F) : Set F

theorem prop_4_15_i {G : Type u_1} [Group G] [TopologicalSpace G] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) [ChartedSpace H G] [LieGroup I ⊤ G] [LocallyCompactSpace G] [SecondCountableTopology G] [T2Space G] [MeasureTheory.MeasureSpace G] [BorelSpace G] [MeasureTheory.volume.IsHaarMeasure] [FiniteDimensional ℝ E] [CompleteSpace F] (π : ContinuousRepresentation G F) : Dense (ContinuousRepresentation.smoothVectors I π)

theorem prop_4_15_ii {G : Type u_1} [Group G] [TopologicalSpace G] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) [ChartedSpace H G] [LieGroup I ⊤ G] (π : ContinuousRepresentation G F) (v : F) (hv : π.IsGFiniteVector v) : ContinuousRepresentation.IsSmoothVector I π v