Distributions and Convolution

This file defines distributions on totally disconnected locally compact Hausdorff spaces, compactly supported distributions on td groups, and convolution with delta and Haar distributions.

structure Distribution_td (X : Type u_1) [TopologicalSpace X] extends CptSupportLocConst_td X →ₗ[ℂ] ℂ : Type u_1

A distribution on X is a ℂ-linear functional on the space of compactly supported locally constant functions.

• toFun : CptSupportLocConst_td X → ℂ
• map_add' (x y : CptSupportLocConst_td X) : self.toFun (x + y) = self.toFun x + self.toFun y
• map_smul' (m : ℂ) (x : CptSupportLocConst_td X) : self.toFun (m • x) = (RingHom.id ℂ) m • self.toFun x

instance Distribution_td.instFunLikeCptSupportLocConst_tdComplex {X : Type u_2} [TopologicalSpace X] : FunLike (Distribution_td X) (CptSupportLocConst_td X) ℂ

Equations

• Distribution_td.instFunLikeCptSupportLocConst_tdComplex = { coe := fun (F : Distribution_td X) => ⇑F.toLinearMap, coe_injective' := ⋯ }

theorem Distribution_td.toFun_eq_coe {X : Type u_2} [TopologicalSpace X] (F : Distribution_td X) : F.toFun = ⇑F

theorem Distribution_td.map_add {X : Type u_2} [TopologicalSpace X] (F : Distribution_td X) (φ ψ : CptSupportLocConst_td X) : F (φ + ψ) = F φ + F ψ

Distributions are additive.

theorem Distribution_td.map_smul {X : Type u_2} [TopologicalSpace X] (F : Distribution_td X) (c : ℂ) (φ : CptSupportLocConst_td X) : F (c • φ) = c * F φ

Distributions are ℂ-linear.

theorem Distribution_td.ext {X : Type u_2} [TopologicalSpace X] {T S : Distribution_td X} (h : ∀ (φ : CptSupportLocConst_td X), T φ = S φ) : T = S

theorem Distribution_td.ext_iff {X : Type u_2} [TopologicalSpace X] {T S : Distribution_td X} : T = S ↔ ∀ (φ : CptSupportLocConst_td X), T φ = S φ

noncomputable def Distribution_td.extendByZero {X : Type u_2} [TopologicalSpace X] (Z : Set X) (f : ↑Z → ℂ) (_hf_lc : IsLocallyConstant f) : X → ℂ

Extend a locally constant function on a subset Z to all of X by setting it to zero outside Z.

Equations

• Distribution_td.extendByZero Z f _hf_lc x = if h : x ∈ Z then f ⟨x, h⟩ else 0

theorem Distribution_td.extendByZero_locallyConstant {X : Type u_2} [TopologicalSpace X] (Z : Set X) (hZ : IsClopen Z) (f : ↑Z → ℂ) (hf_lc : IsLocallyConstant f) : IsLocallyConstant (extendByZero Z f hf_lc)

The extension by zero of a locally constant function is locally constant.

theorem Distribution_td.extendByZero_hasCompactSupport {X : Type u_2} [TopologicalSpace X] (Z : Set X) (hZ_closed : IsClosed Z) (hZ_compact : IsCompact Z) (f : ↑Z → ℂ) (hf_lc : IsLocallyConstant f) (_hf_cs : HasCompactSupport fun (z : ↑Z) => f z) : HasCompactSupport (extendByZero Z f hf_lc)

The extension by zero has compact support if Z is closed and compact.

noncomputable def Distribution_td.restrict {X : Type u_2} [TopologicalSpace X] (F : Distribution_td X) (Z : Set X) (hZ_clopen : IsClopen Z) (hZ_compact : IsCompact Z) (f : ↑Z → ℂ) (hf_lc : IsLocallyConstant f) (hf_cs : HasCompactSupport f) : ℂ

Restriction of a distribution F on X to a subset Z. The restriction sends a function f on Z to F applied to the extension of f by zero.

Equations

• One or more equations did not get rendered due to their size.

def Distribution_td.support {X : Type u_2} [TopologicalSpace X] (F : Distribution_td X) : Set X

The support of a distribution F is the smallest closed set S such that the restriction of F to X \ S is zero.

Equations

• F.support = {x : X | ∀ (U : Set X), IsOpen U → x ∈ U → ∃ (φ : CptSupportLocConst_td X), Function.support ⇑φ ⊆ U ∧ F.toFun φ ≠ 0}

theorem Distribution_td.support_isClosed {X : Type u_2} [TopologicalSpace X] (F : Distribution_td X) : IsClosed F.support

The support of a distribution is closed.

A distribution vanishes on test functions whose support is disjoint from its support.

theorem Distribution_td.apply_eq_zero_of_support_disjoint {X : Type u_2} [TopologicalSpace X] [TotallyDisconnectedSpace X] [T2Space X] (F : Distribution_td X) (φ : CptSupportLocConst_td X) (h : Disjoint F.support (Function.support ⇑φ)) : F φ = 0

Functions and Distributions on a td group

Translations of functions on a td group

def rightTranslate {G : Type u_2} [Group G] (φ : G → ℂ) (g : G) : G → ℂ

Right translation of a function by g: (R_g φ)(x) = φ(xg).

Equations

• rightTranslate φ g x = φ (x * g)

def leftTranslate {G : Type u_2} [Group G] (φ : G → ℂ) (g : G) : G → ℂ

Left translation of a function by g: (L_g φ)(x) = φ(g⁻¹x).

Equations

• leftTranslate φ g x = φ (g⁻¹ * x)

theorem support_rightTranslate {G : Type u_2} [Group G] (φ : G → ℂ) (g : G) : Function.support (rightTranslate φ g) = (fun (x : G) => x * g⁻¹) '' Function.support φ

theorem support_leftTranslate {G : Type u_2} [Group G] (φ : G → ℂ) (g : G) : Function.support (leftTranslate φ g) = (fun (x : G) => g * x) '' Function.support φ

theorem tsupport_rightTranslate {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (φ : G → ℂ) (g : G) : tsupport (rightTranslate φ g) = (fun (x : G) => x * g⁻¹) '' tsupport φ

theorem tsupport_leftTranslate {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (φ : G → ℂ) (g : G) : tsupport (leftTranslate φ g) = (fun (x : G) => g * x) '' tsupport φ

theorem rightTranslate_isLocallyConstant {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {φ : G → ℂ} (hφ : IsLocallyConstant φ) (g : G) : IsLocallyConstant (rightTranslate φ g)

Right translation preserves local constancy.

theorem leftTranslate_isLocallyConstant {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {φ : G → ℂ} (hφ : IsLocallyConstant φ) (g : G) : IsLocallyConstant (leftTranslate φ g)

Left translation preserves local constancy.

theorem rightTranslate_hasCompactSupport {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {φ : G → ℂ} (hφ : HasCompactSupport φ) (g : G) : HasCompactSupport (rightTranslate φ g)

Right translation preserves compact support.

theorem leftTranslate_hasCompactSupport {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {φ : G → ℂ} (hφ : HasCompactSupport φ) (g : G) : HasCompactSupport (leftTranslate φ g)

Left translation preserves compact support.

noncomputable def CptSupportLocConst_td.rightTranslate {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (φ : CptSupportLocConst_td G) (g : G) : CptSupportLocConst_td G

Right translation of a compactly supported locally constant function.

Equations

• φ.rightTranslate g = { toFun := rightTranslate (⇑φ) g, locallyConstant' := ⋯, hasCompactSupport' := ⋯ }

noncomputable def CptSupportLocConst_td.leftTranslate {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (φ : CptSupportLocConst_td G) (g : G) : CptSupportLocConst_td G

Left translation of a compactly supported locally constant function.

Equations

• φ.leftTranslate g = { toFun := leftTranslate (⇑φ) g, locallyConstant' := ⋯, hasCompactSupport' := ⋯ }

@[simp]

theorem CptSupportLocConst_td.rightTranslate_apply {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (φ : CptSupportLocConst_td G) (g x : G) : (φ.rightTranslate g) x = φ (x * g)

@[simp]

theorem CptSupportLocConst_td.leftTranslate_apply {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (φ : CptSupportLocConst_td G) (g x : G) : (φ.leftTranslate g) x = φ (g⁻¹ * x)

theorem CptSupportLocConst_td.rightTranslate_leftTranslate {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (φ : CptSupportLocConst_td G) (g h : G) : (φ.leftTranslate g).rightTranslate h = (φ.rightTranslate h).leftTranslate g

theorem CptSupportLocConst_td.rightTranslate_rightTranslate {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (φ : CptSupportLocConst_td G) (g h : G) : (φ.rightTranslate g).rightTranslate h = φ.rightTranslate (h * g)

Distributions on a td group

structure CptSupportDistribution_td (G : Type u_3) [TopologicalSpace G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] : Type u_3

A compactly supported distribution on G.

• toDistribution_td : Distribution_td G
• hasCompactSupport' : IsCompact self.toDistribution_td.support

instance CptSupportDistribution_td.instFunLikeCptSupportLocConst_tdComplex {G : Type u_3} [TopologicalSpace G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] : FunLike (CptSupportDistribution_td G) (CptSupportLocConst_td G) ℂ

Equations

• CptSupportDistribution_td.instFunLikeCptSupportLocConst_tdComplex = { coe := fun (F : CptSupportDistribution_td G) => F.toDistribution_td.toFun, coe_injective' := ⋯ }

@[simp]

theorem CptSupportDistribution_td.toFun_eq_coe {G : Type u_3} [TopologicalSpace G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (F : CptSupportDistribution_td G) : F.toDistribution_td.toFun = ⇑F

instance CptSupportDistribution_td.instZero {G : Type u_3} [TopologicalSpace G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] : Zero (CptSupportDistribution_td G)

Zero compactly supported distribution.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CptSupportDistribution_td.coe_zero' {G : Type u_3} [TopologicalSpace G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] : ⇑0 = 0

noncomputable def CptSupportDistribution_td.convolveTestFun {G : Type u_3} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (D : CptSupportDistribution_td G) (φ : CptSupportLocConst_td G) : G → ℂ

For a test function φ and distribution D, the function x ↦ D(R_x φ) where R_x is right translation. This function is used to define convolution.

Equations

• D.convolveTestFun φ x = D (φ.rightTranslate x)

theorem CptSupportDistribution_td.convolveTestFun_isLocallyConstant {G : Type u_3} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (F : CptSupportDistribution_td G) (φ : CptSupportLocConst_td G) : _root_.IsLocallyConstant (F.convolveTestFun φ)

The function x ↦ D(R_x φ) is locally constant.

theorem CptSupportDistribution_td.convolveTestFun_hasCompactSupport {G : Type u_3} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (F : CptSupportDistribution_td G) (φ : CptSupportLocConst_td G) : HasCompactSupport (F.convolveTestFun φ)

The function x ↦ D(R_x φ) has compact support when D has compact support.

noncomputable def CptSupportDistribution_td.convolveTestFun' {G : Type u_3} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (F : CptSupportDistribution_td G) (φ : CptSupportLocConst_td G) : CptSupportLocConst_td G

The function x ↦ D(R_x φ) as a compactly supported locally constant function.

Equations

• F.convolveTestFun' φ = { toFun := F.convolveTestFun φ, locallyConstant' := ⋯, hasCompactSupport' := ⋯ }

@[simp]

theorem CptSupportDistribution_td.convolveTestFun'_apply {G : Type u_3} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (F : CptSupportDistribution_td G) (φ : CptSupportLocConst_td G) (x : G) : (F.convolveTestFun' φ) x = F (φ.rightTranslate x)

noncomputable def CptSupportDistribution_td.conv {G : Type u_3} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (F D : CptSupportDistribution_td G) : CptSupportDistribution_td G

Convolution of two compactly supported distributions. (F * D)(φ) = F(x ↦ D(R_x φ)) where R_x is right translation by x.

Equations

• F.conv D = { toDistribution_td := { toFun := fun (φ : CptSupportLocConst_td G) => F (D.convolveTestFun' φ), map_add' := ⋯, map_smul' := ⋯ }, hasCompactSupport' := ⋯ }

theorem CptSupportDistribution_td.conv_assoc {G : Type u_3} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (F D H : CptSupportDistribution_td G) : (F.conv D).conv H = F.conv (D.conv H)

Convolution is associative.

noncomputable def CptSupportDistribution_td.deltaDistribution {G : Type u_4} [TopologicalSpace G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (g : G) : CptSupportDistribution_td G

The delta distribution at g ∈ G: δ_g(φ) = φ(g).

Equations

• CptSupportDistribution_td.deltaDistribution g = { toDistribution_td := { toFun := fun (φ : CptSupportLocConst_td G) => φ g, map_add' := ⋯, map_smul' := ⋯ }, hasCompactSupport' := ⋯ }

@[simp]

theorem CptSupportDistribution_td.deltaDistribution_apply {G : Type u_4} [TopologicalSpace G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (g : G) (φ : CptSupportLocConst_td G) : (deltaDistribution g) φ = φ g

noncomputable def CptSupportDistribution_td.indicatorFunction {G : Type u_4} [TopologicalSpace G] (S : Set G) (hS_clopen : IsClopen S) (hS_compact : IsCompact S) : CptSupportLocConst_td G

The characteristic function of a clopen compact set as a compactly supported locally constant function.

Equations

• CptSupportDistribution_td.indicatorFunction S hS_clopen hS_compact = { toFun := S.indicator fun (x : G) => 1, locallyConstant' := ⋯, hasCompactSupport' := ⋯ }

@[simp]

theorem CptSupportDistribution_td.indicatorFunction_apply {G : Type u_4} [TopologicalSpace G] (S : Set G) (hS_clopen : IsClopen S) (hS_compact : IsCompact S) (g : G) : (indicatorFunction S hS_clopen hS_compact) g = S.indicator (fun (x : G) => 1) g

noncomputable def CptSupportDistribution_td.normalizedHaarDistribution {G : Type u_4} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (H : OpenSubgroup G) (hH_compact : IsCompact ↑H) : CptSupportDistribution_td G

The normalized Haar measure e_H for a compact open subgroup H. For a test function φ, e_H(φ) is the average value of φ over H with respect to the normalized Haar measure on the compact group H.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CptSupportDistribution_td.normalizedHaarDistribution_apply {G : Type u_4} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (H : OpenSubgroup G) (hH_compact : IsCompact ↑H) (φ : CptSupportLocConst_td G) : (normalizedHaarDistribution H hH_compact) φ = ∫ (h : ↥H), φ ↑h ∂MeasureTheory.Measure.haarMeasure ⊤

e_H applied to a test function.

Properties of Haar distribution and delta functions

theorem CptSupportDistribution_td.normalizedHaarDistribution_conv_self {G : Type u_4} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (H : OpenSubgroup G) (hH_compact : IsCompact ↑H) : (normalizedHaarDistribution H hH_compact).conv (normalizedHaarDistribution H hH_compact) = normalizedHaarDistribution H hH_compact

The normalized Haar distribution e_H is idempotent under convolution: e_H * e_H = e_H.

theorem CptSupportDistribution_td.deltaDistribution_conv_normalizedHaar {G : Type u_4} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (g : G) (H : OpenSubgroup G) (hH_compact : IsCompact ↑H) (φ : CptSupportLocConst_td G) : ((deltaDistribution g).conv (normalizedHaarDistribution H hH_compact)) φ = (normalizedHaarDistribution H hH_compact) (φ.rightTranslate g)

Convolution of delta function with normalized Haar distribution: δ_g * e_H(φ) = e_H(R_g φ) for any g ∈ G.

theorem CptSupportDistribution_td.normalizedHaar_conv_deltaDistribution {G : Type u_4} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (g : G) (H : OpenSubgroup G) (hH_compact : IsCompact ↑H) (φ : CptSupportLocConst_td G) : ((normalizedHaarDistribution H hH_compact).conv (deltaDistribution g)) φ = (normalizedHaarDistribution H hH_compact) (φ.leftTranslate g⁻¹)

Convolution of normalized Haar distribution with delta function: e_H * δ_g(φ) = e_H(L_{g⁻¹} φ) for any g ∈ G.

The proof uses that (e_H * δ_g)(φ) = e_H(x ↦ δ_g(R_x φ)) = e_H(x ↦ φ(g * x)) and (L_{g⁻¹} φ)(h) = φ(g * h), so the integrands match.

theorem CptSupportDistribution_td.delta_conv_normalizedHaar_comm {G : Type u_4} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (g : G) (H : OpenSubgroup G) (hH_compact : IsCompact ↑H) (hg : g ∈ H) : (deltaDistribution g).conv (normalizedHaarDistribution H hH_compact) = (normalizedHaarDistribution H hH_compact).conv (deltaDistribution g)

For g ∈ H, δ_g * e_H = e_H * δ_g. This uses the fact that e_H is bi-H-invariant.

Translation actions on distributions

noncomputable def CptSupportDistribution_td.leftTranslate {G : Type u_3} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (F : CptSupportDistribution_td G) (g : G) : CptSupportDistribution_td G

Left translation of a distribution by g: (g · F)(φ) = F(L_{g⁻¹} φ). This gives a left action: g · (h · F) = (gh) · F.

Equations

• F.leftTranslate g = { toDistribution_td := have __LinearMap := CptSupportDistribution_td.leftTranslate_linearMap✝ F g; { toLinearMap := __LinearMap }, hasCompactSupport' := ⋯ }

@[simp]

theorem CptSupportDistribution_td.leftTranslate_apply {G : Type u_3} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (F : CptSupportDistribution_td G) (g : G) (φ : CptSupportLocConst_td G) : (F.leftTranslate g) φ = F (φ.leftTranslate g⁻¹)

noncomputable def CptSupportDistribution_td.rightTranslate {G : Type u_3} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (F : CptSupportDistribution_td G) (g : G) : CptSupportDistribution_td G

Right translation of a distribution by g: (F · g)(φ) = F(R_g φ). This gives a right action: (F · g) · h = F · (gh).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CptSupportDistribution_td.rightTranslate_apply {G : Type u_3} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (F : CptSupportDistribution_td G) (g : G) (φ : CptSupportLocConst_td G) : (F.rightTranslate g) φ = F (φ.rightTranslate g)

theorem CptSupportDistribution_td.leftTranslate_leftTranslate {G : Type u_3} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (F : CptSupportDistribution_td G) (g h : G) : (F.leftTranslate h).leftTranslate g = F.leftTranslate (g * h)

Left translation is a left action: g · (h · F) = (gh) · F.

theorem CptSupportDistribution_td.rightTranslate_rightTranslate {G : Type u_3} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (F : CptSupportDistribution_td G) (g h : G) : (F.rightTranslate g).rightTranslate h = F.rightTranslate (g * h)

Right translation is a right action: (F · g) · h = F · (gh).

def CptSupportDistribution_td.IsLeftInvariant {G : Type u_3} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (F : CptSupportDistribution_td G) (H : OpenSubgroup G) : Prop

A distribution is left H-invariant if h · F = F for all h ∈ H.

Equations

• F.IsLeftInvariant H = ∀ h ∈ H, F.leftTranslate h = F

def CptSupportDistribution_td.IsRightInvariant {G : Type u_3} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (F : CptSupportDistribution_td G) (H : OpenSubgroup G) : Prop

A distribution is right H-invariant if F · h = F for all h ∈ H.

Equations

• F.IsRightInvariant H = ∀ h ∈ H, F.rightTranslate h = F

def CptSupportDistribution_td.IsBiInvariant {G : Type u_3} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (F : CptSupportDistribution_td G) (H : OpenSubgroup G) : Prop

A distribution is bi-H-invariant if it is both left and right H-invariant.

Equations

• F.IsBiInvariant H = (F.IsLeftInvariant H ∧ F.IsRightInvariant H)

theorem CptSupportDistribution_td.IsLeftInvariant.apply {G : Type u_3} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] {F : CptSupportDistribution_td G} {H : OpenSubgroup G} (hF : F.IsLeftInvariant H) {h : G} (hh : h ∈ H) (φ : CptSupportLocConst_td G) : F (φ.leftTranslate h⁻¹) = F φ

theorem CptSupportDistribution_td.IsRightInvariant.apply {G : Type u_3} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] {F : CptSupportDistribution_td G} {H : OpenSubgroup G} (hF : F.IsRightInvariant H) {h : G} (hh : h ∈ H) (φ : CptSupportLocConst_td G) : F (φ.rightTranslate h) = F φ

def CptSupportDistribution_td.IsLocallyConstant {G : Type u_3} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (F : CptSupportDistribution_td G) : Prop

A compactly supported distribution is locally constant if there exists a compact open subgroup H such that F is bi-H-invariant.

Equations

• F.IsLocallyConstant = ∃ (H : OpenSubgroup G), IsCompact ↑H ∧ F.IsBiInvariant H

def CptSupportDistribution_td.IsLeftLocallyConstant {G : Type u_3} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (F : CptSupportDistribution_td G) : Prop

A compactly supported distribution is left locally constant if there exists a compact open subgroup H such that F is left-H-invariant.

Equations

• F.IsLeftLocallyConstant = ∃ (H : OpenSubgroup G), IsCompact ↑H ∧ F.IsLeftInvariant H

def CptSupportDistribution_td.IsRightLocallyConstant {G : Type u_3} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (F : CptSupportDistribution_td G) : Prop

A compactly supported distribution is left locally constant if there exists a compact open subgroup H such that F is right-H-invariant.

Equations

• F.IsRightLocallyConstant = ∃ (H : OpenSubgroup G), IsCompact ↑H ∧ F.IsRightInvariant H

theorem CptSupportDistribution_td.IsLocallyConstant.isLeftLocallyConstant {G : Type u_3} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] {F : CptSupportDistribution_td G} (hF : F.IsLocallyConstant) : F.IsLeftLocallyConstant

theorem CptSupportDistribution_td.IsLocallyConstant.isRightLocallyConstant {G : Type u_3} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] {F : CptSupportDistribution_td G} (hF : F.IsLocallyConstant) : F.IsRightLocallyConstant

theorem CptSupportDistribution_td.normalizedHaarDistribution_isLeftInvariant {G : Type u_4} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (H : OpenSubgroup G) (hH_compact : IsCompact ↑H) : (normalizedHaarDistribution H hH_compact).IsLeftInvariant H

The normalized Haar distribution e_H is left H-invariant.

theorem CptSupportDistribution_td.normalizedHaarDistribution_isRightInvariant {G : Type u_4} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (H : OpenSubgroup G) (hH_compact : IsCompact ↑H) : (normalizedHaarDistribution H hH_compact).IsRightInvariant H

The normalized Haar distribution e_H is right H-invariant.

theorem CptSupportDistribution_td.normalizedHaarDistribution_isBiInvariant {G : Type u_4} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (H : OpenSubgroup G) (hH_compact : IsCompact ↑H) : (normalizedHaarDistribution H hH_compact).IsBiInvariant H

The normalized Haar distribution e_H is bi-H-invariant.

theorem CptSupportDistribution_td.rightCoset_isClopen {G : Type u_4} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (H : OpenSubgroup G) (g : G) : IsClopen ((fun (h : G) => h * g) '' ↑H)

Right cosets of an open subgroup are clopen.

theorem CptSupportDistribution_td.rightCoset_isCompact {G : Type u_4} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (H : OpenSubgroup G) (hH_compact : IsCompact ↑H) (g : G) : IsCompact ((fun (h : G) => h * g) '' ↑H)

Right cosets of a compact subgroup are compact.

theorem CptSupportDistribution_td.exists_finite_rightCoset_cover {G : Type u_4} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (H : OpenSubgroup G) (K : Set G) (hK : IsCompact K) : ∃ (n : ℕ) (g : Fin n → G), K ⊆ ⋃ (i : Fin n), (fun (h : G) => h * g i) '' ↑H

A compact set is covered by finitely many right cosets of an open subgroup.

noncomputable def CptSupportDistribution_td.rightCosetIndicator {G : Type u_4} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (H : OpenSubgroup G) (hH_compact : IsCompact ↑H) (g : G) : CptSupportLocConst_td G

The indicator function of a right coset.

Equations

• CptSupportDistribution_td.rightCosetIndicator H hH_compact g = CptSupportDistribution_td.indicatorFunction ((fun (h : G) => h * g) '' ↑H) ⋯ ⋯

noncomputable def CptSupportDistribution_td.cosetAverage {G : Type u_4} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (H : OpenSubgroup G) (hH_compact : IsCompact ↑H) (g : G) (φ : CptSupportLocConst_td G) : ℂ

The average value of a test function on a right coset Hg, computed using the normalized Haar measure on H.

Equations

• CptSupportDistribution_td.cosetAverage H hH_compact g φ = ∫ (h : ↥H), φ (↑h * g) ∂MeasureTheory.Measure.haarMeasure ⊤

theorem CptSupportDistribution_td.IsLeftInvariant.apply_leftTranslate {G : Type u_4} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] {F : CptSupportDistribution_td G} {H : OpenSubgroup G} (hF : F.IsLeftInvariant H) (h : G) (hh : h ∈ H) (φ : CptSupportLocConst_td G) : F (φ.leftTranslate h⁻¹) = F φ

Left H-invariance implies F(L_{h⁻¹} φ) = F(φ) for h ∈ H.

theorem CptSupportDistribution_td.IsLeftInvariant.integral_leftTranslate {G : Type u_4} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] {F : CptSupportDistribution_td G} {H : OpenSubgroup G} (hH_compact : IsCompact ↑H) (hF : F.IsLeftInvariant H) (φ : CptSupportLocConst_td G) : ∫ (h : ↥H), F (φ.leftTranslate (↑h)⁻¹) ∂MeasureTheory.Measure.haarMeasure ⊤ = F φ

For a left H-invariant distribution, the integral of F(L_h φ) over h ∈ H equals F(φ).

theorem CptSupportDistribution_td.IsLeftInvariant.apply_zero_average {G : Type u_4} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] {F : CptSupportDistribution_td G} {H : OpenSubgroup G} (hH_compact : IsCompact ↑H) (hF : F.IsLeftInvariant H) (g : G) (φ : CptSupportLocConst_td G) (hφ_supp : Function.support ⇑φ ⊆ (fun (h : G) => h * g) '' ↑H) (hφ_avg : cosetAverage H hH_compact g φ = 0) : F φ = 0

For a left H-invariant distribution F and φ supported on Hg with zero average, F(φ) = 0. This is the key technical lemma for the coset decomposition.

theorem CptSupportDistribution_td.biInvariant_coset_determined {G : Type u_4} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (H : OpenSubgroup G) (hH_compact : IsCompact ↑H) (F : CptSupportDistribution_td G) (hF_biinv : F.IsBiInvariant H) (g : G) (φ : CptSupportLocConst_td G) (hφ_supp : Function.support ⇑φ ⊆ (fun (h : G) => h * g) '' ↑H) : ∃ (c : ℂ), F φ = c * F (rightCosetIndicator H hH_compact g)

For a bi-H-invariant distribution F and the indicator function of a right coset Hg, the value F(χ_{Hg}) determines F's action on functions supported on that coset.

theorem CptSupportDistribution_td.biInvariant_distribution_decomposition {G : Type u_4} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (H : OpenSubgroup G) (hH_compact : IsCompact ↑H) (F : CptSupportDistribution_td G) (hF_biinv : F.IsBiInvariant H) : ∃ (n : ℕ) (g : Fin n → G) (a : Fin n → ℂ), ∀ (φ : CptSupportLocConst_td G), F φ = ∑ i : Fin n, a i * ((normalizedHaarDistribution H hH_compact).conv (deltaDistribution (g i))) φ

Structure theorem: Any H-invariant compactly supported distribution can be written as a finite sum of e_H * δ_{g_i} for some g_i ∈ G.

If F is bi-H-invariant and compactly supported, then there exist g₁, ..., gₖ ∈ G and a₁, ..., aₖ ∈ ℂ such that F = ∑ᵢ aᵢ (e_H * δ_{gᵢ}).

theorem CptSupportDistribution_td.IsLeftLocallyConstant.isRightLocallyConstant {G : Type u_4} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] {F : CptSupportDistribution_td G} : F.IsLeftLocallyConstant → F.IsRightLocallyConstant

Left locally constant implies right locally constant.

theorem CptSupportDistribution_td.IsRightLocallyConstant.isLeftLocallyConstant {G : Type u_4} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] {F : CptSupportDistribution_td G} : F.IsRightLocallyConstant → F.IsLeftLocallyConstant

Right locally constant implies left locally constant. This is symmetric to IsLeftLocallyConstant.isRightLocallyConstant.