Local Steinhaus product-neighborhood conclusion

Open

QAlgorithms.Papers.Independent.Intakethird100.P08.proposition6

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$ .

Then $MM$ contains an open identity neighborhood:

\exists\ V\subseteq E\text{ open},\quad e\in V\subseteq MM=\{xy:x,y\in M\}.

This turns finite positive mass in a controlled local region into a topological neighborhood.

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]

/-- Proposition 6, PDF p. 18: the local Steinhaus product-neighborhood
conclusion, on the preimage of U rather than on U itself. -/
theorem proposition6 (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) :
    ∃ V : Set (ExtensionPoint D), IsOpen V ∧ identityPoint D ∈ V ∧
      V ⊆ {z | ∃ x ∈ M, ∃ y ∈ M, actionTwistedMul D x y = z} := by sorry

end ConstructedExtension

end QAlgorithms.Papers.Independent.Intakethird100.P08

Source

On Cohomology theory for topological groups, arXiv:1009.4519v1, PDF p. 18, Proposition 6: local Steinhaus product-neighborhood conclusion

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, such that $\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 there exists an open set $V\subseteq E$ containing $(0,1)$ such that every $z\in V$ can be written $z=x\star y$ for some $x,y\in M$ .

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