theorem
ContinuousRep.smoothVector_zero
{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)
:
IsSmoothVector I π 0
theorem
ContinuousRep.smoothVector_add
{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 w : F}
(hv : IsSmoothVector I π v)
(hw : IsSmoothVector I π w)
:
IsSmoothVector I π (v + w)
theorem
ContinuousRep.smoothVector_smul
{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)
(c : ℂ)
{v : F}
(hv : IsSmoothVector I π v)
:
IsSmoothVector I π (c • v)
theorem
ContinuousRep.contDiffWithinAt_deriv_parametric
{E₀ : Type u_5}
{F₀ : Type u_6}
[NormedAddCommGroup E₀]
[NormedSpace ℝ E₀]
[NormedAddCommGroup F₀]
[NormedSpace ℝ F₀]
{f : E₀ → ℝ → F₀}
{s : Set E₀}
{e₀ : E₀}
{y₀ : ℝ}
(hf : ContDiffWithinAt ℝ (↑⊤) (Function.uncurry f) (s ×ˢ Set.univ) (e₀, y₀))
(he₀ : e₀ ∈ s)
:
ContDiffWithinAt ℝ (↑⊤) (fun (e : E₀) => deriv (f e) y₀) s e₀
theorem
ContinuousRep.derivedRep_maps_smooth
{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)
(lieExp : E → G)
(hExp : ContMDiff (modelWithCornersSelf ℝ E) I ⊤ lieExp)
(hExp1 : lieExp 0 = 1)
(b : E)
(v : F)
(hv : IsSmoothVector I π v)
:
IsSmoothVector I π (π.derivedRep lieExp b v)
theorem
ContinuousRep.contDiff_orbitMap_comp_lieExp
{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)
(lieExp : E → G)
(hExp : ContMDiff (modelWithCornersSelf ℝ E) I ⊤ lieExp)
(v : F)
(hv : IsSmoothVector I π v)
:
ContDiff ℝ ↑⊤ fun (x : E) => (π.toMonoidHom (lieExp x)) v
theorem
ContinuousRep.derivedRep_eq_fderiv
{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)
(lieExp : E → G)
(hExp : ContMDiff (modelWithCornersSelf ℝ E) I ⊤ lieExp)
(v : F)
(b : E)
(hv : IsSmoothVector I π v)
:
theorem
ContinuousRep.derivedRep_linear
{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)
(lieExp : E → G)
(hExp : ContMDiff (modelWithCornersSelf ℝ E) I ⊤ lieExp)
(_hExp1 : lieExp 0 = 1)
(v : F)
(hv : IsSmoothVector I π v)
:
IsLinearMap ℝ fun (b : E) => π.derivedRep lieExp b v
theorem
ContinuousRep.derivedRep_bracket
{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]
[LieRing E]
[LieAlgebra ℝ E]
(π : ContinuousRep G F)
(lieExp : E → G)
(hExp : ContMDiff (modelWithCornersSelf ℝ E) I ⊤ lieExp)
(hExp1 : lieExp 0 = 1)
(hExpAdd : ∀ (X : E) (t s : ℝ), lieExp ((t + s) • X) = lieExp (t • X) * lieExp (s • X))
(h_bracket :
∀ (X Y : E),
⁅X, Y⁆ = (fderiv ℝ
(fun (s : ℝ) =>
(fderiv ℝ
(fun (t : ℝ) =>
↑(extChartAt I 1) (lieExp (t • X) * lieExp (s • Y) * (lieExp (t • X))⁻¹ * (lieExp (s • Y))⁻¹))
0)
1)
0)
1)
(X Y : E)
(v : F)
(hv : IsSmoothVector I π v)
:
π.derivedRep lieExp ⁅X, Y⁆ v = π.derivedRep lieExp X (π.derivedRep lieExp Y v) - π.derivedRep lieExp Y (π.derivedRep lieExp X v)
noncomputable def
ContinuousRep.repOfFunction
{G : Type u_3}
[Group G]
[TopologicalSpace G]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℂ F]
[MeasureTheory.MeasureSpace G]
(π : ContinuousRep G F)
(f : G → ℂ)
(v : F)
:
F
Instances For
def
ContinuousRep.IsSmoothCompactlySupportedFunction
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
(I : ModelWithCorners ℝ E H)
{G : Type u_3}
[TopologicalSpace G]
[ChartedSpace H G]
(f : G → ℂ)
:
Instances For
def
ContinuousRep.gardingSubspace
{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]
[MeasureTheory.MeasureSpace G]
(π : ContinuousRep G F)
:
Instances For
theorem
ContinuousRep.contDiffOn_convolution_chartCoord
{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]
[MeasureTheory.MeasureSpace G]
[CompleteSpace F]
[FiniteDimensional ℝ E]
[T2Space G]
[MeasurableMul G]
[MeasureTheory.volume.IsMulLeftInvariant]
[BorelSpace G]
[SecondCountableTopology G]
[LocallyCompactSpace G]
(f : G → ℂ)
(hf : IsSmoothCompactlySupportedFunction I f)
(w : G → F)
(x₀ : G)
:
ContDiffOn ℝ (↑⊤) (fun (x : E) => ∫ (g : G), f ((↑(extChartAt I x₀).symm x)⁻¹ * g) • w g) (extChartAt I x₀).target
theorem
ContinuousRep.contMDiff_convolution_integral
{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]
[MeasureTheory.MeasureSpace G]
[CompleteSpace F]
[FiniteDimensional ℝ E]
[T2Space G]
[MeasurableMul G]
[MeasureTheory.volume.IsMulLeftInvariant]
[BorelSpace G]
[SecondCountableTopology G]
[LocallyCompactSpace G]
(f : G → ℂ)
(hf : IsSmoothCompactlySupportedFunction I f)
(w : G → F)
:
theorem
ContinuousRep.continuous_lieGroup_convolution
{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]
[MeasureTheory.MeasureSpace G]
[CompleteSpace F]
[FiniteDimensional ℝ E]
[T2Space G]
[MeasurableMul G]
[MeasureTheory.volume.IsMulLeftInvariant]
[BorelSpace G]
[SecondCountableTopology G]
[LocallyCompactSpace G]
(f : G → ℂ)
(hf : IsSmoothCompactlySupportedFunction I f)
(w : G → F)
:
theorem
ContinuousRep.contDiffOn_lieGroup_convolution_chartCoord
{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]
[MeasureTheory.MeasureSpace G]
[CompleteSpace F]
[FiniteDimensional ℝ E]
[T2Space G]
[MeasurableMul G]
[MeasureTheory.volume.IsMulLeftInvariant]
[BorelSpace G]
[SecondCountableTopology G]
[LocallyCompactSpace G]
(f : G → ℂ)
(hf : IsSmoothCompactlySupportedFunction I f)
(w : G → F)
(x₀ : G)
(y₀ : F)
:
ContDiffOn ℝ (↑⊤)
(↑(extChartAt (modelWithCornersSelf ℝ F) y₀) ∘ (fun (h : G) => ∫ (g : G), f (h⁻¹ * g) • w g) ∘ ↑(extChartAt I x₀).symm)
((extChartAt I x₀).target ∩ ↑(extChartAt I x₀).symm ⁻¹' ((fun (h : G) => ∫ (g : G), f (h⁻¹ * g) • w g) ⁻¹' (extChartAt (modelWithCornersSelf ℝ F) y₀).source))
theorem
ContinuousRep.orbitMap_gardingVector_eq
{G : Type u_3}
[Group G]
[TopologicalSpace G]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℂ F]
[MeasureTheory.MeasureSpace G]
[CompleteSpace F]
[MeasurableMul G]
[MeasureTheory.volume.IsMulLeftInvariant]
(π : ContinuousRep G F)
(f : G → ℂ)
(v : F)
(h : G)
(hint : MeasureTheory.Integrable (fun (g : G) => f g • (π.toMonoidHom g) v) MeasureTheory.volume)
:
theorem
ContinuousRep.gardingVector_isSmooth
{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]
[MeasureTheory.MeasureSpace G]
[CompleteSpace F]
[FiniteDimensional ℝ E]
[T2Space G]
[MeasurableMul G]
[MeasureTheory.volume.IsMulLeftInvariant]
[BorelSpace G]
[SecondCountableTopology G]
[LocallyCompactSpace G]
(π : ContinuousRep G F)
(f : G → ℂ)
(hf : IsSmoothCompactlySupportedFunction I f)
(v : F)
:
IsSmoothVector I π (π.repOfFunction f v)
theorem
ContinuousRep.exists_smooth_dirac_sequence
{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]
[MeasureTheory.MeasureSpace G]
[FiniteDimensional ℝ E]
[T2Space G]
[BorelSpace G]
[SecondCountableTopology G]
[LocallyCompactSpace G]
[MeasureTheory.volume.IsHaarMeasure]
:
theorem
ContinuousRep.smooth_dirac_convolution_tendsto
{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]
[MeasureTheory.MeasureSpace G]
[CompleteSpace F]
[T2Space G]
[BorelSpace G]
[SecondCountableTopology G]
[LocallyCompactSpace G]
(π : ContinuousRep G F)
[MeasureTheory.volume.IsHaarMeasure]
(v : F)
(φ : ℕ → G → ℂ)
(hφsmooth : ∀ (n : ℕ), IsSmoothCompactlySupportedFunction I (φ n))
(hφnonneg : ∀ (n : ℕ) (g : G), (φ n g).im = 0 ∧ 0 ≤ (φ n g).re)
(hφnorm : ∀ (n : ℕ), ∫ (g : G), (φ n g).re = 1)
(hφshrink : ∀ U ∈ nhds 1, ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → Function.support (φ n) ⊆ U)
:
Filter.Tendsto (fun (n : ℕ) => π.repOfFunction (φ n) v) Filter.atTop (nhds v)
theorem
ContinuousRep.exists_gardingVector_tendsto
{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]
[MeasureTheory.MeasureSpace G]
[CompleteSpace F]
[FiniteDimensional ℝ E]
[T2Space G]
[BorelSpace G]
[SecondCountableTopology G]
[LocallyCompactSpace G]
(π : ContinuousRep G F)
[MeasureTheory.volume.IsHaarMeasure]
(v : F)
:
∃ (φ : ℕ → G → ℂ),
(∀ (n : ℕ), IsSmoothCompactlySupportedFunction I (φ n)) ∧ Filter.Tendsto (fun (n : ℕ) => π.repOfFunction (φ n) v) Filter.atTop (nhds v)
theorem
ContinuousRep.gardingSubspace_dense
{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]
[MeasureTheory.MeasureSpace G]
[CompleteSpace F]
[FiniteDimensional ℝ E]
[T2Space G]
[BorelSpace G]
[SecondCountableTopology G]
[LocallyCompactSpace G]
(π : ContinuousRep G F)
[MeasureTheory.volume.IsHaarMeasure]
:
Dense ↑(gardingSubspace I π)
noncomputable def
ContinuousRep.leftInvariantDeriv
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{G : Type u_3}
[Group G]
(lieExp : E → G)
(X : E)
(f : G → ℂ)
(g : G)
:
Instances For
theorem
ContinuousRep.derivedRep_gardingVector
{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]
[MeasureTheory.MeasureSpace G]
[CompleteSpace F]
[MeasurableMul G]
[MeasureTheory.volume.IsMulLeftInvariant]
(π : ContinuousRep G F)
(lieExp : E → G)
(hExp : ContMDiff (modelWithCornersSelf ℝ E) I ⊤ lieExp)
(hExp1 : lieExp 0 = 1)
(X : E)
(f : G → ℂ)
(v : F)
(hf : IsSmoothCompactlySupportedFunction I f)
:
theorem
ContinuousRep.contMDiff_orbitMap_of_finiteDimensional
{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]
{W : Submodule ℂ F}
[FiniteDimensional ℂ ↥W]
(ρ : G →* ↥W →L[ℂ] ↥W)
(hρ_cont : Continuous fun (p : G × ↥W) => (ρ p.1) p.2)
(w : ↥W)
:
ContMDiff I (modelWithCornersSelf ℝ F) ↑⊤ fun (g : G) => ↑((ρ g) w)
theorem
ContinuousRep.lieGroup_finiteDimOrbit_smooth_orbitMap
{E : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_6}
[TopologicalSpace H]
(I : ModelWithCorners ℝ E H)
{G : Type u_7}
[Group G]
[TopologicalSpace G]
[ChartedSpace H G]
[LieGroup I ⊤ G]
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace ℂ F]
(π : G →* F →L[ℂ] F)
(hπ_cont : Continuous fun (p : G × F) => (π p.1) p.2)
(v : F)
(hfin : FiniteDimensional ℂ ↥(Submodule.span ℂ (Set.range fun (g : G) => (π g) v)))
:
ContMDiff I (modelWithCornersSelf ℝ F) ↑⊤ fun (g : G) => (π g) v
theorem
ContinuousRep.finDimRep_orbitMap_smooth
{E : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_6}
[TopologicalSpace H]
(I : ModelWithCorners ℝ E H)
{G : Type u_7}
[Group G]
[TopologicalSpace G]
[ChartedSpace H G]
[LieGroup I ⊤ G]
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace ℂ F]
(π : G →* F →L[ℂ] F)
(hπ_cont : Continuous fun (p : G × F) => (π p.1) p.2)
(v : F)
(hfin : FiniteDimensional ℂ ↥(Submodule.span ℂ (Set.range fun (g : G) => (π g) v)))
:
ContMDiff I (modelWithCornersSelf ℝ F) ↑⊤ fun (g : G) => (π g) v
theorem
ContinuousRep.orbitMap_smooth_of_finiteDim_span
{E : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_6}
[TopologicalSpace H]
(I : ModelWithCorners ℝ E H)
{G : Type u_7}
[Group G]
[TopologicalSpace G]
[ChartedSpace H G]
[LieGroup I ⊤ G]
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace ℂ F]
(π : ContinuousRep G F)
(v : F)
(hfin : FiniteDimensional ℂ ↥(Submodule.span ℂ (Set.range fun (g : G) => (π.toMonoidHom g) v)))
:
ContMDiff I (modelWithCornersSelf ℝ F) (↑⊤) (π.orbitMap v)
theorem
ContinuousRep.kfinite_le_smooth
{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)
: