Uniform continuity on compact subsets of the constructed space

Open

QAlgorithms.Papers.Independent.Intakethird100.P08.lemma4

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 $f:E\to\mathbb R$ be continuous, let $\varepsilon>0$ , and let $C\subseteq E$ be compact. There is a neighborhood $V$ of $e$ such that

x,y\in C,\quad x^{-1}y\in V\quad\Longrightarrow\quad |f(x)-f(y)|<\varepsilon.

The assertion supplies compact-set uniform continuity without a pre-assumed uniform group structure.

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 4, PDF p. 15: compact-set uniform continuity for the constructed
space, before global group continuity is known. Empty compact sets are permitted. -/
theorem lemma4 (D : LocalCocycle G A) (f : ExtensionPoint D → ℝ)
    (hf : Continuous f) (eps : ℝ) (heps : 0 < eps)
    (C : Set (ExtensionPoint D)) (hC : IsCompact C) :
    ∃ V : Set (ExtensionPoint D), V ∈ nhds (identityPoint D) ∧
      ∀ x ∈ C, ∀ y ∈ C, actionTwistedMul D (twistedInv D x) y ∈ V →
        |f x - f y| < eps := by sorry

end ConstructedExtension

end QAlgorithms.Papers.Independent.Intakethird100.P08

Source

On Cohomology theory for topological groups, arXiv:1009.4519v1, PDF p. 15, Lemma 4: uniform continuity on compact sets before global group 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 additive abelian topological group, both with their Borel measurable structures. Let $D$ specify additive automorphisms $\alpha_p$ , with $\alpha_1=\mathrm{id}$ , $\alpha_{pq}=\alpha_p\circ\alpha_q$ , and jointly continuous evaluation; a measurable function $\kappa:G\times G\to A$ satisfying $\alpha_p(\kappa(q,r))+\kappa(p,qr)=\kappa(p,q)+\kappa(pq,r)$ and $\kappa(1,p)=\kappa(p,1)=0$ ; and an open neighborhood $U_0$ of $1$ such that $\kappa$ is continuous on $U_0^2$ . Put $E=A\times G$ , define $(a,p)\star(b,q)=(a+\alpha_p(b)+\kappa(p,q),pq)$ , and give $E$ the topology generated by $z\star(U_A\times U_G)$ for $z\in E$ , open $U_A\ni0$ , and open $U_G\ni1$ such that $\kappa$ is continuous on $U_G^2$ . Define $e=(0,1)$ and $x^\dagger=(\alpha_{p^{-1}}(-(a+\kappa(p,p^{-1}))),p^{-1})$ for $x=(a,p)$ . For every continuous function $f:E\to\mathbb R$ , every real number $\varepsilon>0$ , and every compact set $C\subseteq E$ , there exists a neighborhood $V$ of $e$ such that

x,y\in C\ \text{and}\ x^\dagger\star y\in V \quad\Longrightarrow\quad |f(x)-f(y)|<\varepsilon.

Here a neighborhood need only contain an open set containing $e$ ; $V$ itself need not be open. No support or sign condition is imposed on $f$ . The compact set $C$ may be empty, in which case the condition on $x,y$ is vacuous.

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