Global continuity of the local convolution function

Open

QAlgorithms.Papers.Independent.Intakethird100.P08.lemma7

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $G$ be a Hausdorff locally compact second-countable topological group and let $A$ be a Hausdorff locally compact second-countable abelian topological group with a continuous action of $G$ by automorphisms, written $g\cdot a$ . Let $F:G\times G\to A$ be a Borel measurable two-cocycle, with pointwise identity

F(g,h)+F(gh,k)=g\cdot F(h,k)+F(g,hk),\qquad F(1,g)=F(g,1)=0.

Assume that $F$ is continuous on $U_F\times U_F$ , where $U_F$ is an open identity neighborhood. Let $E=A\times_F G$ , with multiplication $(a,g)(b,h)=(a+g\cdot b+F(g,h),gh)$ and inverse $(a,g)^{-1}=(-g^{-1}\cdot(a+F(g,g^{-1})),g^{-1})$ . Equip $E$ with the topology generated by left translates of the rectangles $U_A\times U_G$ , where $U_A,U_G$ are open identity neighborhoods and $F$ is continuous on $U_G\times U_G$ . Write $e=(0,1)$ and $\pi(a,g)=g$ .

Let $\mu$ be a nonzero Borel measure on $E$ with the properties obtained in Remark 4: it is finite on compact sets, and $\mu(xW)=\mu(W)$ for every $x\in E$ and Borel $W$ whose closure is compact.

Let $U_2\subseteq G$ be a symmetric relatively compact open identity neighborhood satisfying $\overline{U_2}\,\overline{U_2}\subseteq U_F$ . Let $M\subseteq E$ be Borel measurable and symmetric, with $e\in M$ , $M\subseteq\pi^{-1}(U_2)$ , and $0<\mu(M)<\infty$ .

Define $u:E\to\mathbb R$ by $u(x)=\mu(M\cap xM)$ , using the real value of this finite mass. Then

\mu(M\cap xM)<\infty\quad(x\in E),\qquad u\text{ is continuous on all of }E.

The finite-mass bound makes the real-valued convolution well-defined, and the conclusion is global continuity.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P08

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P08

open Set MeasureTheory

open scoped BigOperators Topology CompactlySupported

section ConstructedExtension

variable {G A : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [T2Space G] [LocallyCompactSpace G] [SecondCountableTopology G]
  [MeasurableSpace G] [BorelSpace G]
  [AddCommGroup A] [TopologicalSpace A] [IsTopologicalAddGroup A]
  [T2Space A] [LocallyCompactSpace A] [SecondCountableTopology A]
  [MeasurableSpace A] [BorelSpace A]

/-- Lemma 7, PDF pp. 19--21: global continuity of u(x)=mu(M intersect xM).
The explicit finite-mass clause justifies toReal; no infinite mass is silently
converted to zero. The proof's dropped projection on p. 19 is not propagated. -/
theorem lemma7 (D : LocalCocycle G A) (mu : Measure (ExtensionPoint D))
    (hmu : IsLeftInvariantMeasure D mu) (U : Set G) (M : Set (ExtensionPoint D))
    (hM : IsLocalSteinhausSet D mu U M) :
    (∀ x : ExtensionPoint D, mu (M ∩ (actionTwistedMul D x) '' M) < ⊤) ∧
    Continuous (localConvolution D mu M) := by sorry

end ConstructedExtension

end QAlgorithms.Papers.Independent.Intakethird100.P08

Source

On Cohomology theory for topological groups, arXiv:1009.4519v1, PDF p. 19, Lemma 7: convolution continuity

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

Let $G$ be a Hausdorff, locally compact, second countable topological group, and let $A$ be a Hausdorff, locally compact, second countable topological abelian group, both equipped with their Borel measurable structures. Let $D$ specify additive automorphisms $\rho_g$ of $A$ satisfying $\rho_1=\mathrm{id}$ , $\rho_{gh}=\rho_g\circ\rho_h$ , and joint continuity of $(g,a)\mapsto\rho_g(a)$ ; a measurable function $c:G\times G\to A$ satisfying $\rho_g(c(h,k))+c(g,hk)=c(g,h)+c(gh,k)$ and $c(1,g)=c(g,1)=0$ ; and an open neighborhood $N$ of $1$ on whose square $c$ is continuous. On $E=A\times G$ , define $(a,g)\star(b,h)=(a+\rho_g(b)+c(g,h),gh)$ and $(a,g)^\dagger=(\rho_{g^{-1}}(-(a+c(g,g^{-1}))),g^{-1})$ . Equip $E$ with the topology generated by all sets $\{x\star(a,g):a\in P,\ g\in Q\}$ , where $x\in E$ , $P$ is an open neighborhood of $0$ , $Q$ is an open neighborhood of $1$ , and $c$ is continuous on $Q\times Q$ , and use its Borel measurable structure. Suppose $\mu$ is a nonzero measure on $E$ , finite on every compact subset, satisfying $\mu(\{x\star w:w\in W\})=\mu(W)$ for every $x\in E$ and every measurable $W$ with compact closure. Let $U\subseteq G$ and $M\subseteq E$ satisfy: $M$ is measurable; $x\in M$ if and only if $x^\dagger\in M$ for every $x$ ; every $(a,g)\in M$ has $g\in U$ ; $U$ is open, contains $1$ , and satisfies $g\in U$ if and only if $g^{-1}\in U$ for every $g$ ; $\overline U$ is compact; $gh\in N$ for every $g,h\in\overline U$ ; $(0,1)\in M$ ; and $0<\mu(M)<\infty$ . Then, for every $x\in E$ , $\mu(M\cap\{x\star y:y\in M\})<\infty$ , and the real-valued function sending $x$ to this measure converted to a real number is continuous on all of $E$ . The conversion retains every finite value and sends infinity to $0$ ; the asserted finiteness excludes the latter case here.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph