structure PlancherelCompact.IrrFinDimRep (K : Type u_1) [Group K] [TopologicalSpace K] [CompactSpace K] : Type (max 1 u_1)

• carrier : Type
• instNormedAddCommGroup : NormedAddCommGroup self.carrier
• instInnerProductSpace : InnerProductSpace ℂ self.carrier
• instFiniteDimensional : FiniteDimensional ℂ self.carrier
• instCompleteSpace : CompleteSpace self.carrier
• rep : ContinuousRep K self.carrier
• irred : self.rep.IsIrreducible
• unitary : self.rep.IsUnitary
• nontrivial : Nontrivial self.carrier

noncomputable def PlancherelCompact.IrrFinDimRep.dim {K : Type u_1} [Group K] [TopologicalSpace K] [CompactSpace K] (ρ : IrrFinDimRep K) : ℕ

noncomputable def PlancherelCompact.IrrFinDimRep.repFourierCoeff {K : Type u_1} [Group K] [TopologicalSpace K] [CompactSpace K] [MeasureTheory.MeasureSpace K] (ρ : IrrFinDimRep K) (f : K → ℂ) : ρ.carrier →L[ℂ] ρ.carrier

noncomputable def PlancherelCompact.IrrFinDimRep.plancherelTerm {K : Type u_1} [Group K] [TopologicalSpace K] [CompactSpace K] [MeasureTheory.MeasureSpace K] (ρ : IrrFinDimRep K) (f₁ f₂ : K → ℂ) : ℂ

noncomputable def PlancherelCompact.IrrFinDimRep.plancherelSingleTerm {K : Type u_1} [Group K] [TopologicalSpace K] [CompactSpace K] [MeasureTheory.MeasureSpace K] (ρ : IrrFinDimRep K) (f : K → ℂ) : ℂ

@[reducible, inline]

abbrev PlancherelCompact.PeterWeylIndex {K : Type u_1} [Group K] [TopologicalSpace K] [CompactSpace K] (ι : Type u_2) (ρ : ι → IrrFinDimRep K) : Type u_2

noncomputable def PlancherelCompact.peterWeyl_orthonormal_basis {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] [MeasureTheory.MeasureSpace K] [BorelSpace K] [MeasureTheory.volume.IsHaarMeasure] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (ι : Type u_2) (ρ : ι → IrrFinDimRep K) (hρ_surj : ∀ (σ : IrrFinDimRep K), ∃ (i : ι), Nonempty (RepEquiv σ.rep (ρ i).rep)) (hρ_inj : ∀ (i j : ι), Nonempty (RepEquiv (ρ i).rep (ρ j).rep) → i = j) : HilbertBasis (PeterWeylIndex ι ρ) ℂ ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

theorem PlancherelCompact.peterWeyl_basis_sum_eq_plancherelTerm {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] [MeasureTheory.MeasureSpace K] [BorelSpace K] [MeasureTheory.volume.IsHaarMeasure] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (ι : Type u_2) (ρ : ι → IrrFinDimRep K) (hρ_surj : ∀ (σ : IrrFinDimRep K), ∃ (i : ι), Nonempty (RepEquiv σ.rep (ρ i).rep)) (hρ_inj : ∀ (i j : ι), Nonempty (RepEquiv (ρ i).rep (ρ j).rep) → i = j) (f₁ f₂ : K → ℂ) (hf₁ : MeasureTheory.MemLp f₁ 2 MeasureTheory.volume) (hf₂ : MeasureTheory.MemLp f₂ 2 MeasureTheory.volume) (i : ι) : have b := peterWeyl_orthonormal_basis ι ρ hρ_surj hρ_inj; ∑' (jk : Fin (ρ i).dim × Fin (ρ i).dim), inner ℂ (MeasureTheory.MemLp.toLp f₂ hf₂) (b ⟨i, jk⟩) * inner ℂ (b ⟨i, jk⟩) (MeasureTheory.MemLp.toLp f₁ hf₁) = (ρ i).plancherelTerm f₁ f₂

theorem PlancherelCompact.proposition_4_1_plancherel_hasSum {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] [MeasureTheory.MeasureSpace K] [BorelSpace K] [MeasureTheory.volume.IsHaarMeasure] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {ι : Type u_2} {ρ : ι → IrrFinDimRep K} (hρ_surj : ∀ (σ : IrrFinDimRep K), ∃ (i : ι), Nonempty (RepEquiv σ.rep (ρ i).rep)) (hρ_inj : ∀ (i j : ι), Nonempty (RepEquiv (ρ i).rep (ρ j).rep) → i = j) (f₁ f₂ : K → ℂ) (hf₁ : MeasureTheory.MemLp f₁ 2 MeasureTheory.volume) (hf₂ : MeasureTheory.MemLp f₂ 2 MeasureTheory.volume) : HasSum (fun (i : ι) => (ρ i).plancherelTerm f₁ f₂) (inner ℂ (MeasureTheory.MemLp.toLp f₂ hf₂) (MeasureTheory.MemLp.toLp f₁ hf₁))

noncomputable def PlancherelCompact.convolutionOp {K : Type u_1} [Group K] [TopologicalSpace K] [CompactSpace K] [MeasureTheory.MeasureSpace K] (f ψ : K → ℂ) : K → ℂ

def PlancherelCompact.convolutionKernel {K : Type u_1} [Group K] (f : K → ℂ) : K → K → ℂ

theorem PlancherelCompact.convolutionOp_eq_kernel_integral {K : Type u_1} [Group K] [TopologicalSpace K] [CompactSpace K] [MeasureTheory.MeasureSpace K] (f ψ : K → ℂ) (x : K) : convolutionOp f ψ x = ∫ (y : K), convolutionKernel f x y * ψ y

@[simp]

theorem PlancherelCompact.convolutionKernel_diag_eq {K : Type u_1} [Group K] (f : K → ℂ) (x : K) : convolutionKernel f x x = f 1

noncomputable def PlancherelCompact.convolutionKernelDiagIntegral {K : Type u_1} [Group K] [TopologicalSpace K] [CompactSpace K] [MeasureTheory.MeasureSpace K] (f : K → ℂ) : ℂ

theorem PlancherelCompact.convolutionKernelDiag_eq_const {K : Type u_1} [Group K] [TopologicalSpace K] [CompactSpace K] [MeasureTheory.MeasureSpace K] (f : K → ℂ) : convolutionKernelDiagIntegral f = ∫ (x : K), f 1

theorem PlancherelCompact.convolutionKernelDiagIntegral_eq_eval_one {K : Type u_1} [Group K] [TopologicalSpace K] [CompactSpace K] [MeasureTheory.MeasureSpace K] [BorelSpace K] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (f : K → ℂ) : convolutionKernelDiagIntegral f = f 1

noncomputable def PlancherelCompact.convolutionOperatorTrace {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] [MeasureTheory.MeasureSpace K] [BorelSpace K] [MeasureTheory.volume.IsHaarMeasure] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (f : K → ℂ) : ℂ

theorem PlancherelCompact.lidskiiMercer_trace_eq_diagIntegral {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] [MeasureTheory.MeasureSpace K] [BorelSpace K] [MeasureTheory.volume.IsHaarMeasure] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (f : K → ℂ) (hf : Continuous f) : convolutionOperatorTrace f = convolutionKernelDiagIntegral f

theorem PlancherelCompact.peterWeyl_spectral_hasSum_trace {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] [MeasureTheory.MeasureSpace K] [BorelSpace K] [MeasureTheory.volume.IsHaarMeasure] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (ι : Type u_2) (ρ : ι → IrrFinDimRep K) (hρ_surj : ∀ (σ : IrrFinDimRep K), ∃ (i : ι), Nonempty (RepEquiv σ.rep (ρ i).rep)) (hρ_inj : ∀ (i j : ι), Nonempty (RepEquiv (ρ i).rep (ρ j).rep) → i = j) (f : K → ℂ) (hf : Continuous f) : HasSum (fun (i : ι) => (ρ i).plancherelSingleTerm f) (convolutionOperatorTrace f)

theorem PlancherelCompact.peterWeyl_spectral_trace_hasSum {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] [MeasureTheory.MeasureSpace K] [BorelSpace K] [MeasureTheory.volume.IsHaarMeasure] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (ι : Type u_2) (ρ : ι → IrrFinDimRep K) (hρ_surj : ∀ (σ : IrrFinDimRep K), ∃ (i : ι), Nonempty (RepEquiv σ.rep (ρ i).rep)) (hρ_inj : ∀ (i j : ι), Nonempty (RepEquiv (ρ i).rep (ρ j).rep) → i = j) (f : K → ℂ) (hf : Continuous f) : HasSum (fun (i : ι) => (ρ i).plancherelSingleTerm f) (convolutionKernelDiagIntegral f)

theorem PlancherelCompact.plancherel_formula {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] [MeasureTheory.MeasureSpace K] [BorelSpace K] [MeasureTheory.volume.IsHaarMeasure] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {EK : Type u_2} [NormedAddCommGroup EK] [NormedSpace ℝ EK] {HK : Type u_3} [TopologicalSpace HK] (IK : ModelWithCorners ℝ EK HK) [ChartedSpace HK K] [LieGroup IK ⊤ K] (ι : Type u_4) (ρ : ι → IrrFinDimRep K) (hρ_surj : ∀ (σ : IrrFinDimRep K), ∃ (i : ι), Nonempty (RepEquiv σ.rep (ρ i).rep)) (hρ_inj : ∀ (i j : ι), Nonempty (RepEquiv (ρ i).rep (ρ j).rep) → i = j) (f : K → ℂ) (hf : ContMDiff IK (modelWithCornersSelf ℝ ℂ) ⊤ f) : f 1 = ∑' (i : ι), (ρ i).plancherelSingleTerm f

theorem PlancherelCompact.plancherel_formula_summable {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] [MeasureTheory.MeasureSpace K] [BorelSpace K] [MeasureTheory.volume.IsHaarMeasure] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {EK : Type u_2} [NormedAddCommGroup EK] [NormedSpace ℝ EK] {HK : Type u_3} [TopologicalSpace HK] (IK : ModelWithCorners ℝ EK HK) [ChartedSpace HK K] [LieGroup IK ⊤ K] (ι : Type u_4) (ρ : ι → IrrFinDimRep K) (hρ_surj : ∀ (σ : IrrFinDimRep K), ∃ (i : ι), Nonempty (RepEquiv σ.rep (ρ i).rep)) (hρ_inj : ∀ (i j : ι), Nonempty (RepEquiv (ρ i).rep (ρ j).rep) → i = j) (f : K → ℂ) (hf : ContMDiff IK (modelWithCornersSelf ℝ ℂ) ⊤ f) : Summable fun (i : ι) => ‖(ρ i).plancherelSingleTerm f‖

theorem PlancherelCompact.exists_dirac_sequence {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [SecondCountableTopology G] [MeasureTheory.MeasureSpace G] [BorelSpace G] [MeasureTheory.volume.IsHaarMeasure] : ∃ (φ : ℕ → G → ℝ), (∀ (n : ℕ), Continuous (φ n)) ∧ (∀ (n : ℕ), HasCompactSupport (φ n)) ∧ ∀ (f : G → ℂ), Continuous f → HasCompactSupport f → Filter.Tendsto (fun (n : ℕ) => ∫ (g : G), ↑(φ n g) * f g) Filter.atTop (nhds (f 1))

theorem PlancherelCompact.exists_smooth_dirac_sequence {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [SecondCountableTopology G] [MeasureTheory.MeasureSpace G] [BorelSpace G] [MeasureTheory.volume.IsHaarMeasure] {EG : Type u_2} [NormedAddCommGroup EG] [NormedSpace ℝ EG] [FiniteDimensional ℝ EG] {HG : Type u_3} [TopologicalSpace HG] (IG : ModelWithCorners ℝ EG HG) [ChartedSpace HG G] [LieGroup IG ⊤ G] [T2Space G] : ∃ (φ : ℕ → G → ℝ), (∀ (n : ℕ), ContMDiff IG (modelWithCornersSelf ℝ ℝ) (↑⊤) (φ n)) ∧ (∀ (n : ℕ), HasCompactSupport (φ n)) ∧ ∀ (f : G → ℂ), Continuous f → HasCompactSupport f → Filter.Tendsto (fun (n : ℕ) => ∫ (g : G), ↑(φ n g) * f g) Filter.atTop (nhds (f 1))

theorem PlancherelCompact.cc_seq_converges_to_dirac {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [SecondCountableTopology G] [MeasureTheory.MeasureSpace G] [BorelSpace G] [MeasureTheory.volume.IsHaarMeasure] (g₀ : G) : ∃ (ψ : ℕ → G → ℝ), (∀ (n : ℕ), Continuous (ψ n)) ∧ (∀ (n : ℕ), HasCompactSupport (ψ n)) ∧ ∀ (f : G → ℂ), Continuous f → HasCompactSupport f → Filter.Tendsto (fun (n : ℕ) => ∫ (g : G), ↑(ψ n g) * f g) Filter.atTop (nhds (f g₀))

theorem PlancherelCompact.concreteDiracEmbed_apply_eq' {X : Type u_1} [TopologicalSpace X] (σ : X →₀ ℂ) (f : C(X, ℂ)) : ((concreteDiracEmbed X) σ) f = ∑ x ∈ σ.support, σ x * f x

theorem PlancherelCompact.finitely_supported_seq_dense_in_measures {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] [SecondCountableTopology X] [T2Space X] (μ : C(X, ℂ) →L[ℂ] ℂ) : ∃ (μ_seq : ℕ → C(X, ℂ) →L[ℂ] ℂ), (∀ (n : ℕ), ∃ (S : Finset X) (c : X → ℂ), ∀ (f : C(X, ℂ)), (μ_seq n) f = ∑ x ∈ S, c x * f x) ∧ ∀ (f : C(X, ℂ)), Filter.Tendsto (fun (n : ℕ) => (μ_seq n) f) Filter.atTop (nhds (μ f))

theorem PlancherelCompact.compactly_supported_measure_to_clm {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [SecondCountableTopology G] [T2Space G] [MeasureTheory.MeasureSpace G] [BorelSpace G] [MeasureTheory.volume.IsHaarMeasure] (μ : MeasureTheory.Measure G) [MeasureTheory.IsFiniteMeasureOnCompacts μ] (hμ : IsCompact μ.support) : ∃ (Φ : C(G, ℂ) →L[ℂ] ℂ), ∀ (f : C(G, ℂ)), Φ f = ∫ (g : G), f g ∂μ

theorem PlancherelCompact.cc_seq_dense_approx_finsupp {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [SecondCountableTopology G] [T2Space G] [MeasureTheory.MeasureSpace G] [BorelSpace G] [MeasureTheory.volume.IsHaarMeasure] (μ : MeasureTheory.Measure G) [MeasureTheory.IsFiniteMeasureOnCompacts μ] (hμ : IsCompact μ.support) : ∃ (S : ℕ → Finset G) (c : ℕ → G → ℂ), ∀ (f : G → ℂ), Continuous f → Filter.Tendsto (fun (n : ℕ) => ∑ x ∈ S n, c n x * f x) Filter.atTop (nhds (∫ (g : G), f g ∂μ))

theorem PlancherelCompact.hasCompactSupport_finset_sum' {α : Type u_1} {β : Type u_2} {ι : Type u_3} [TopologicalSpace α] [AddCommMonoid β] [TopologicalSpace β] {F : Finset ι} {f : ι → α → β} (hf : ∀ i ∈ F, HasCompactSupport (f i)) : HasCompactSupport fun (x : α) => ∑ i ∈ F, f i x

theorem PlancherelCompact.finsupp_in_seq_closure_cc {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [SecondCountableTopology G] [MeasureTheory.MeasureSpace G] [BorelSpace G] [MeasureTheory.volume.IsHaarMeasure] (dirac_approx : ∀ (g₀ : G), ∃ (ψ : ℕ → G → ℝ), (∀ (n : ℕ), Continuous (ψ n)) ∧ (∀ (n : ℕ), HasCompactSupport (ψ n)) ∧ ∀ (f : G → ℂ), Continuous f → HasCompactSupport f → Filter.Tendsto (fun (n : ℕ) => ∫ (g : G), ↑(ψ n g) * f g) Filter.atTop (nhds (f g₀))) (F : Finset G) (a : G → ℂ) : ∃ (ψ : ℕ → G → ℂ), (∀ (n : ℕ), Continuous (ψ n)) ∧ (∀ (n : ℕ), HasCompactSupport (ψ n)) ∧ ∀ (f : G → ℂ), Continuous f → HasCompactSupport f → Filter.Tendsto (fun (n : ℕ) => ∫ (g : G), ψ n g * f g) Filter.atTop (nhds (∑ x ∈ F, a x * f x))

theorem PlancherelCompact.simultaneous_diagonal_extraction (F : ℕ → ℕ → ℕ → ℂ) (a : ℕ → ℕ → ℂ) (b : ℕ → ℂ) (hF : ∀ (k n : ℕ), Filter.Tendsto (F k n) Filter.atTop (nhds (a k n))) (ha : ∀ (k : ℕ), Filter.Tendsto (a k) Filter.atTop (nhds (b k))) : ∃ (m : ℕ → ℕ), ∀ (k : ℕ), Filter.Tendsto (fun (n : ℕ) => F k n (m n)) Filter.atTop (nhds (b k))

theorem PlancherelCompact.exists_countable_cc_determining {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [SecondCountableTopology G] [MeasureTheory.MeasureSpace G] [BorelSpace G] [MeasureTheory.volume.IsHaarMeasure] : ∃ (funs : ℕ → G → ℂ), (∀ (k : ℕ), Continuous (funs k)) ∧ (∀ (k : ℕ), HasCompactSupport (funs k)) ∧ ∀ (φ : ℕ → G → ℂ) (L : (G → ℂ) → ℂ), (∀ (n : ℕ), HasCompactSupport (φ n)) → (∀ (k : ℕ), Filter.Tendsto (fun (n : ℕ) => ∫ (g : G), φ n g * funs k g) Filter.atTop (nhds (L (funs k)))) → ∀ (f : G → ℂ), Continuous f → HasCompactSupport f → Filter.Tendsto (fun (n : ℕ) => ∫ (g : G), φ n g * f g) Filter.atTop (nhds (L f))

theorem PlancherelCompact.seq_closure_diagonal_extraction {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [SecondCountableTopology G] [MeasureTheory.MeasureSpace G] [BorelSpace G] [MeasureTheory.volume.IsHaarMeasure] (ψ : ℕ → ℕ → G → ℂ) (hcont : ∀ (n m : ℕ), Continuous (ψ n m)) (hsupp : ∀ (n m : ℕ), HasCompactSupport (ψ n m)) (L_n : ℕ → (G → ℂ) → ℂ) (hinner : ∀ (n : ℕ) (f : G → ℂ), Continuous f → HasCompactSupport f → Filter.Tendsto (fun (m : ℕ) => ∫ (g : G), ψ n m g * f g) Filter.atTop (nhds (L_n n f))) (L : (G → ℂ) → ℂ) (houter : ∀ (f : G → ℂ), Continuous f → Filter.Tendsto (fun (n : ℕ) => L_n n f) Filter.atTop (nhds (L f))) : ∃ (m : ℕ → ℕ), (∀ (n : ℕ), Continuous (ψ n (m n))) ∧ (∀ (n : ℕ), HasCompactSupport (ψ n (m n))) ∧ ∀ (f : G → ℂ), Continuous f → HasCompactSupport f → Filter.Tendsto (fun (n : ℕ) => ∫ (g : G), ψ n (m n) g * f g) Filter.atTop (nhds (L f))

theorem PlancherelCompact.cc_seq_dense_diag {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [SecondCountableTopology G] [MeasureTheory.MeasureSpace G] [BorelSpace G] [MeasureTheory.volume.IsHaarMeasure] (dirac_approx : ∀ (g₀ : G), ∃ (ψ : ℕ → G → ℝ), (∀ (n : ℕ), Continuous (ψ n)) ∧ (∀ (n : ℕ), HasCompactSupport (ψ n)) ∧ ∀ (f : G → ℂ), Continuous f → HasCompactSupport f → Filter.Tendsto (fun (n : ℕ) => ∫ (g : G), ↑(ψ n g) * f g) Filter.atTop (nhds (f g₀))) (μ : MeasureTheory.Measure G) (S : ℕ → Finset G) (c : ℕ → G → ℂ) (hconv : ∀ (f : G → ℂ), Continuous f → Filter.Tendsto (fun (n : ℕ) => ∑ x ∈ S n, c n x * f x) Filter.atTop (nhds (∫ (g : G), f g ∂μ))) : ∃ (ψ : ℕ → G → ℂ), (∀ (n : ℕ), Continuous (ψ n)) ∧ (∀ (n : ℕ), HasCompactSupport (ψ n)) ∧ ∀ (f : G → ℂ), Continuous f → HasCompactSupport f → Filter.Tendsto (fun (n : ℕ) => ∫ (g : G), ψ n g * f g) Filter.atTop (nhds (∫ (g : G), f g ∂μ))

theorem PlancherelCompact.cc_seq_dense_in_measures {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [SecondCountableTopology G] [T2Space G] [MeasureTheory.MeasureSpace G] [BorelSpace G] [MeasureTheory.volume.IsHaarMeasure] (μ : MeasureTheory.Measure G) [MeasureTheory.IsFiniteMeasureOnCompacts μ] (hμ : IsCompact μ.support) : ∃ (ψ : ℕ → G → ℂ), (∀ (n : ℕ), Continuous (ψ n)) ∧ (∀ (n : ℕ), HasCompactSupport (ψ n)) ∧ ∀ (f : G → ℂ), Continuous f → HasCompactSupport f → Filter.Tendsto (fun (n : ℕ) => ∫ (g : G), ψ n g * f g) Filter.atTop (nhds (∫ (g : G), f g ∂μ))

theorem PlancherelCompact.cc_seq_dense_in_measures_weakstar {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [SecondCountableTopology G] [T2Space G] [MeasureTheory.MeasureSpace G] [BorelSpace G] [MeasureTheory.volume.IsHaarMeasure] (μ : WeakDual ℂ C(G, ℂ)) : ∃ (ψ : ℕ → C(G, ℂ)), ∀ (f : C(G, ℂ)), Filter.Tendsto (fun (n : ℕ) => ∫ (x : G), (ψ n) x * f x) Filter.atTop (nhds (μ f))

theorem PlancherelCompact.cc_seq_dense_in_measures_of_measure {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [LocallyCompactSpace G] [SecondCountableTopology G] [T2Space G] [MeasureTheory.MeasureSpace G] [BorelSpace G] [MeasureTheory.volume.IsHaarMeasure] (μ : MeasureTheory.Measure G) [MeasureTheory.IsFiniteMeasureOnCompacts μ] (hμ : IsCompact μ.support) : ∃ (ψ : ℕ → C(G, ℂ)), ∀ (f : C(G, ℂ)), Filter.Tendsto (fun (n : ℕ) => ∫ (x : G), (ψ n) x * f x) Filter.atTop (nhds (∫ (x : G), f x ∂μ))

theorem PlancherelCompact.smooth_cc_seq_converges_to_dirac {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [SecondCountableTopology G] [MeasureTheory.MeasureSpace G] [BorelSpace G] [MeasureTheory.volume.IsHaarMeasure] {EG : Type u_2} [NormedAddCommGroup EG] [NormedSpace ℝ EG] [FiniteDimensional ℝ EG] {HG : Type u_3} [TopologicalSpace HG] (IG : ModelWithCorners ℝ EG HG) [ChartedSpace HG G] [LieGroup IG ⊤ G] [T2Space G] (g₀ : G) : ∃ (ψ : ℕ → G → ℝ), (∀ (n : ℕ), ContMDiff IG (modelWithCornersSelf ℝ ℝ) (↑⊤) (ψ n)) ∧ (∀ (n : ℕ), HasCompactSupport (ψ n)) ∧ ∀ (f : G → ℂ), Continuous f → HasCompactSupport f → Filter.Tendsto (fun (n : ℕ) => ∫ (g : G), ↑(ψ n g) * f g) Filter.atTop (nhds (f g₀))

theorem PlancherelCompact.smooth_cc_seq_dense_in_measures {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [SecondCountableTopology G] [MeasureTheory.MeasureSpace G] [BorelSpace G] [MeasureTheory.volume.IsHaarMeasure] {EG : Type u_2} [NormedAddCommGroup EG] [NormedSpace ℝ EG] [FiniteDimensional ℝ EG] {HG : Type u_3} [TopologicalSpace HG] (IG : ModelWithCorners ℝ EG HG) [ChartedSpace HG G] [LieGroup IG ⊤ G] [T2Space G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsFiniteMeasureOnCompacts μ] (hμ : IsCompact μ.support) : ∃ (ψ : ℕ → G → ℂ), (∀ (n : ℕ), ContMDiff IG (modelWithCornersSelf ℝ ℂ) (↑⊤) (ψ n)) ∧ (∀ (n : ℕ), HasCompactSupport (ψ n)) ∧ ∀ (f : G → ℂ), Continuous f → HasCompactSupport f → Filter.Tendsto (fun (n : ℕ) => ∫ (g : G), ψ n g * f g) Filter.atTop (nhds (∫ (g : G), f g ∂μ))

theorem PlancherelCompact.kfinite_dense_in_rep {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] {V : Type u_2} [AddCommGroup V] [Module ℂ V] [TopologicalSpace V] (π : ContinuousRep K V) : Dense ↑(π.kFiniteSubspace ⊤)

def PlancherelCompact.IsKFiniteFunction (K : Type u_1) [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] (f : K → ℂ) : Prop

theorem PlancherelCompact.matrixCoefficient_continuous {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] {W : Type u_2} [AddCommGroup W] [Module ℂ W] [TopologicalSpace W] (ρ : ContinuousRep K W) (φ : W →L[ℂ] ℂ) (v : W) : Continuous (ContinuousRep.matrixCoefficient K ρ φ v)

theorem PlancherelCompact.isKFiniteFunction_continuous {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] (p : K → ℂ) (hp : IsKFiniteFunction K p) : Continuous p

noncomputable def PlancherelCompact.leftRegularRep_CK (K : Type u_1) [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] : ContinuousRep K C(K, ℂ)

@[simp]

theorem PlancherelCompact.leftRegularRep_CK_apply_val {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] (g : K) (f : C(K, ℂ)) (x : K) : (((leftRegularRep_CK K).toMonoidHom g) f) x = f (g⁻¹ * x)

theorem PlancherelCompact.leftRegularRep_eval_identity {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] (f : C(K, ℂ)) (g : K) : f g = (((leftRegularRep_CK K).toMonoidHom g⁻¹) f) 1

noncomputable def PlancherelCompact.contragredientFinRep {V : Type u_1} [AddCommGroup V] [Module ℂ V] (K : Type u_2) [Group K] [TopologicalSpace K] [CompactSpace K] (ρ : Representation ℂ K V) [FiniteDimensional ℂ V] : Representation ℂ K (V →ₗ[ℂ] ℂ)

@[simp]

theorem PlancherelCompact.contragredientFinRep_apply {V : Type u_1} [AddCommGroup V] [Module ℂ V] (K : Type u_2) [Group K] [TopologicalSpace K] [CompactSpace K] (ρ : Representation ℂ K V) [FiniteDimensional ℂ V] (k : K) (φ : V →ₗ[ℂ] ℂ) (v : V) : (((contragredientFinRep K ρ) k) φ) v = φ ((ρ k⁻¹) v)

theorem PlancherelCompact.orbit_span_invariant_of_monoidHom {G : Type u_1} {V : Type u_2} [Group G] [AddCommGroup V] [Module ℂ V] [TopologicalSpace V] (π : G →* V →L[ℂ] V) (K : Subgroup G) (v : V) (g : G) (hg : g ∈ K) (w : V) (hw : w ∈ Submodule.span ℂ (Set.range fun (k : ↥K) => (π ↑k) v)) : (π g) w ∈ Submodule.span ℂ (Set.range fun (k : ↥K) => (π ↑k) v)

theorem PlancherelCompact.isKFinite_leftReg_implies_isKFiniteFunction (K : Type u_1) [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] (p : C(K, ℂ)) (hp : (leftRegularRep_CK K).IsKFinite ⊤ p) : IsKFiniteFunction K ⇑p

theorem PlancherelCompact.kfinite_functions_uniformly_dense {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] (f : C(K, ℂ)) (ε : ℝ) (hε : ε > 0) : ∃ (p : K → ℂ), IsKFiniteFunction K p ∧ ∀ (g : K), ‖f g - p g‖ < ε

theorem PlancherelCompact.kfinite_dense_in_continuous {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] (f : C(K, ℂ)) (ε : ℝ) (hε : ε > 0) : ∃ (p : K → ℂ), IsKFiniteFunction K p ∧ Continuous p ∧ ∀ (g : K), ‖f g - p g‖ < ε

theorem PlancherelCompact.kfinite_dense_in_continuous_dense {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] : Dense {f : C(K, ℂ) | IsKFiniteFunction K ⇑f}

theorem PlancherelCompact.kfinite_subspace_dense_in_CK {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] : Dense ↑((leftRegularRep_CK K).kFiniteSubspace ⊤)

theorem PlancherelCompact.auto_smooth_finiteDim_rep_orbit {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] {EK : Type u_2} [NormedAddCommGroup EK] [NormedSpace ℝ EK] {HK : Type u_3} [TopologicalSpace HK] (IK : ModelWithCorners ℝ EK HK) [ChartedSpace HK K] [LieGroup IK ⊤ K] {W : Type u_4} [AddCommGroup W] [Module ℂ W] [TopologicalSpace W] [FiniteDimensional ℂ W] (ρ_hom : K →* W →L[ℂ] W) (h_cont : Continuous fun (p : K × W) => (ρ_hom p.1) p.2) (φ : W →L[ℂ] ℂ) (v : W) : ContMDiff IK (modelWithCornersSelf ℝ ℂ) ⊤ fun (g : K) => φ ((ρ_hom g) v)

theorem PlancherelCompact.matrixCoefficient_contMDiff {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] {EK : Type u_2} [NormedAddCommGroup EK] [NormedSpace ℝ EK] {HK : Type u_3} [TopologicalSpace HK] (IK : ModelWithCorners ℝ EK HK) [ChartedSpace HK K] [LieGroup IK ⊤ K] {W : Type u_4} [AddCommGroup W] [Module ℂ W] [TopologicalSpace W] [FiniteDimensional ℂ W] (ρ : ContinuousRep K W) (φ : W →L[ℂ] ℂ) (v : W) : ContMDiff IK (modelWithCornersSelf ℝ ℂ) ⊤ (ContinuousRep.matrixCoefficient K ρ φ v)

theorem PlancherelCompact.isKFiniteFunction_contMDiff {K : Type uK} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] {EK : Type uEK} [NormedAddCommGroup EK] [NormedSpace ℝ EK] {HK : Type uHK} [TopologicalSpace HK] (IK : ModelWithCorners ℝ EK HK) [ChartedSpace HK K] [LieGroup IK ⊤ K] (p : K → ℂ) (hp : IsKFiniteFunction K p) : ContMDiff IK (modelWithCornersSelf ℝ ℂ) ⊤ p

theorem PlancherelCompact.leftRegularRep_ck_isContinuousRep {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] {EK : Type u_2} [NormedAddCommGroup EK] [NormedSpace ℝ EK] {HK : Type u_3} [TopologicalSpace HK] (IK : ModelWithCorners ℝ EK HK) [ChartedSpace HK K] [LieGroup IK ⊤ K] (m : ℕ) : ∃ (V : Type) (x : AddCommGroup V) (x_1 : Module ℂ V) (x_2 : TopologicalSpace V) (π : ContinuousRep K V) (emb : V → K → ℂ) (_ : Function.Injective emb), (∀ (k : K) (v : V), emb ((π.toMonoidHom k) v) = fun (x : K) => emb v (k⁻¹ * x)) ∧ (∀ (f : K → ℂ), ContMDiff IK (modelWithCornersSelf ℝ ℂ) ⊤ f → ∃ (v : V), emb v = f) ∧ (∀ (f : K → ℂ), ContMDiff IK (modelWithCornersSelf ℝ ℂ) ⊤ f → ∀ ε > 0, ∀ (v : V), emb v = f → ∃ (U : Set V), v ∈ U ∧ IsOpen U ∧ ∀ w ∈ U, ∀ (g : K), ∀ j ≤ m, ‖iteratedFDeriv ℝ j (writtenInExtChartAt IK (modelWithCornersSelf ℝ ℂ) g f - writtenInExtChartAt IK (modelWithCornersSelf ℝ ℂ) g (emb w)) (↑(extChartAt IK g) g)‖ < ε) ∧ ∀ v ∈ ↑(π.kFiniteSubspace ⊤), IsKFiniteFunction K (emb v)

theorem PlancherelCompact.kfinite_uniform_to_ck_dense {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] {EK : Type u_2} [NormedAddCommGroup EK] [NormedSpace ℝ EK] {HK : Type u_3} [TopologicalSpace HK] (IK : ModelWithCorners ℝ EK HK) [ChartedSpace HK K] [LieGroup IK ⊤ K] (f : K → ℂ) (hf : ContMDiff IK (modelWithCornersSelf ℝ ℂ) ⊤ f) (h_uniform_dense : ∀ δ > 0, ∃ (q : K → ℂ), IsKFiniteFunction K q ∧ ∀ (g : K), ‖f g - q g‖ < δ) (h_smooth : ∀ (q : K → ℂ), IsKFiniteFunction K q → ContMDiff IK (modelWithCornersSelf ℝ ℂ) ⊤ q) (m : ℕ) (ε : ℝ) (hε : ε > 0) : ∃ (p : K → ℂ), IsKFiniteFunction K p ∧ ∀ (g : K), ∀ j ≤ m, ‖iteratedFDeriv ℝ j (writtenInExtChartAt IK (modelWithCornersSelf ℝ ℂ) g f - writtenInExtChartAt IK (modelWithCornersSelf ℝ ℂ) g p) (↑(extChartAt IK g) g)‖ < ε

theorem PlancherelCompact.kfinite_ck_dense {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] {EK : Type u_2} [NormedAddCommGroup EK] [NormedSpace ℝ EK] {HK : Type u_3} [TopologicalSpace HK] (IK : ModelWithCorners ℝ EK HK) [ChartedSpace HK K] [LieGroup IK ⊤ K] (f : K → ℂ) (hf : ContMDiff IK (modelWithCornersSelf ℝ ℂ) ⊤ f) (m : ℕ) (ε : ℝ) (hε : ε > 0) : ∃ (p : K → ℂ), IsKFiniteFunction K p ∧ ∀ (g : K), ∀ j ≤ m, ‖iteratedFDeriv ℝ j (writtenInExtChartAt IK (modelWithCornersSelf ℝ ℂ) g f - writtenInExtChartAt IK (modelWithCornersSelf ℝ ℂ) g p) (↑(extChartAt IK g) g)‖ < ε

theorem PlancherelCompact.kfinite_functions_smooth_dense {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] {EK : Type u_2} [NormedAddCommGroup EK] [NormedSpace ℝ EK] {HK : Type u_3} [TopologicalSpace HK] (IK : ModelWithCorners ℝ EK HK) [ChartedSpace HK K] [LieGroup IK ⊤ K] (f : K → ℂ) (hf : ContMDiff IK (modelWithCornersSelf ℝ ℂ) ⊤ f) (m : ℕ) (ε : ℝ) (hε : ε > 0) : ∃ (p : K → ℂ), IsKFiniteFunction K p ∧ ContMDiff IK (modelWithCornersSelf ℝ ℂ) ⊤ p ∧ ∀ (g : K), ∀ j ≤ m, ‖iteratedFDeriv ℝ j (writtenInExtChartAt IK (modelWithCornersSelf ℝ ℂ) g f - writtenInExtChartAt IK (modelWithCornersSelf ℝ ℂ) g p) (↑(extChartAt IK g) g)‖ < ε

theorem PlancherelCompact.kfinite_dense_in_smooth {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] {EK : Type u_2} [NormedAddCommGroup EK] [NormedSpace ℝ EK] {HK : Type u_3} [TopologicalSpace HK] (IK : ModelWithCorners ℝ EK HK) [ChartedSpace HK K] [LieGroup IK ⊤ K] (f : K → ℂ) (hf : ContMDiff IK (modelWithCornersSelf ℝ ℂ) ⊤ f) (m : ℕ) (ε : ℝ) (hε : ε > 0) : ∃ (p : K → ℂ), IsKFiniteFunction K p ∧ ContMDiff IK (modelWithCornersSelf ℝ ℂ) ⊤ p ∧ ∀ (g : K), ∀ j ≤ m, ‖iteratedFDeriv ℝ j (writtenInExtChartAt IK (modelWithCornersSelf ℝ ℂ) g f - writtenInExtChartAt IK (modelWithCornersSelf ℝ ℂ) g p) (↑(extChartAt IK g) g)‖ < ε

theorem PlancherelCompact.irreducible_rep_finiteDimensional {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] {W : Type u_2} [AddCommGroup W] [Module ℂ W] [TopologicalSpace W] [IsTopologicalAddGroup W] [ContinuousSMul ℂ W] [T2Space W] (π : ContinuousRep K W) (hirr : π.IsIrreducible) : FiniteDimensional ℂ W

@[reducible, inline]

abbrev PlancherelCompact.IsSmoothVector {G : Type u_1} [Group G] [TopologicalSpace G] {EG : Type u_2} [NormedAddCommGroup EG] [NormedSpace ℝ EG] {HG : Type u_3} [TopologicalSpace HG] (IG : ModelWithCorners ℝ EG HG) [ChartedSpace HG G] [LieGroup IG ⊤ G] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (v : F) : Prop

@[reducible, inline]

abbrev PlancherelCompact.smoothVectors {G : Type u_1} [Group G] [TopologicalSpace G] {EG : Type u_2} [NormedAddCommGroup EG] [NormedSpace ℝ EG] {HG : Type u_3} [TopologicalSpace HG] (IG : ModelWithCorners ℝ EG HG) [ChartedSpace HG G] [LieGroup IG ⊤ G] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) : Submodule ℂ F

theorem PlancherelCompact.derivedRep_preserves_smooth {G : Type u_1} [Group G] [TopologicalSpace G] {EG : Type u_2} [NormedAddCommGroup EG] [NormedSpace ℝ EG] {HG : Type u_3} [TopologicalSpace HG] (IG : ModelWithCorners ℝ EG HG) [ChartedSpace HG G] [LieGroup IG ⊤ G] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] (π : ContinuousRep G F) (lieExp : EG → G) (hExp : ContMDiff (modelWithCornersSelf ℝ EG) IG ⊤ lieExp) (hExp1 : lieExp 0 = 1) (b : EG) (v : F) (hv : ContinuousRep.IsSmoothVector IG π v) : ContinuousRep.IsSmoothVector IG π (π.derivedRep lieExp b v)

theorem PlancherelCompact.derivedRep_lie_algebra_hom {G : Type u_1} [Group G] [TopologicalSpace G] {EG : Type u_2} [NormedAddCommGroup EG] [NormedSpace ℝ EG] [LieRing EG] [LieAlgebra ℝ EG] {HG : Type u_3} [TopologicalSpace HG] (IG : ModelWithCorners ℝ EG HG) [ChartedSpace HG G] [LieGroup IG ⊤ G] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] (π : ContinuousRep G F) (lieExp : EG → G) (hExp : ContMDiff (modelWithCornersSelf ℝ EG) IG ⊤ lieExp) (hExp1 : lieExp 0 = 1) (hExpAdd : ∀ (X : EG) (t s : ℝ), lieExp ((t + s) • X) = lieExp (t • X) * lieExp (s • X)) (X Y : EG) (v : F) (hv : ContinuousRep.IsSmoothVector IG π v) : π.derivedRep lieExp ⁅X, Y⁆ v = π.derivedRep lieExp X (π.derivedRep lieExp Y v) - π.derivedRep lieExp Y (π.derivedRep lieExp X v)

theorem PlancherelCompact.smooth_vectors_dense {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [SecondCountableTopology G] [MeasureTheory.MeasureSpace G] [BorelSpace G] [MeasureTheory.volume.IsHaarMeasure] {EG : Type u_2} [NormedAddCommGroup EG] [NormedSpace ℝ EG] [FiniteDimensional ℝ EG] {HG : Type u_3} [TopologicalSpace HG] (IG : ModelWithCorners ℝ EG HG) [ChartedSpace HG G] [LieGroup IG ⊤ G] [T2Space G] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] (π : ContinuousRep G F) : Dense ↑(ContinuousRep.smoothSubspace IG π)

theorem PlancherelCompact.kfinite_subset_smooth {G : Type u_1} [Group G] [TopologicalSpace G] {EG : Type u_2} [NormedAddCommGroup EG] [NormedSpace ℝ EG] {HG : Type u_3} [TopologicalSpace HG] (IG : ModelWithCorners ℝ EG HG) [ChartedSpace HG G] [LieGroup IG ⊤ G] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] (π : ContinuousRep G F) (v : F) (hv : π.IsKFinite ⊤ v) : ContinuousRep.IsSmoothVector IG π v