Finite domination by positive multiples of translates

Open

QAlgorithms.Papers.Independent.Intakethird100.P08.lemma2

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

Write $C_c^+(E)$ for the nonnegative real continuous functions with compact support, where support means the closure of the nonzero locus. For $x\in E$ put $f_x(s)=f(xs)$ .

If $f,g\in C_c^+(E)$ and $g\ne0$ , there are finitely many $c_j>0$ and $u_j\in E$ such that

f(s)\le\sum_{j=1}^r c_jg(u_js)\qquad\text{for every }s\in E.

This makes the defining set of approximate-integral costs nonempty.

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 2, PDF p. 14: domination by finitely many positive multiples of
left translates. The source's reference to Proposition (6) means this constructed E. -/
theorem lemma2 (D : LocalCocycle G A) (f g : ExtensionPoint D → ℝ)
    (hf : IsNonnegativeTest D f) (hg : IsNonnegativeTest D g) (hg0 : g ≠ 0) :
    ∃ (n : ℕ) (c : Fin n → ℝ) (u : Fin n → ExtensionPoint D),
      (∀ j, 0 < c j) ∧
      ∀ s, f s ≤ ∑ j, c j * g (actionTwistedMul D (u j) s) := by sorry

end ConstructedExtension

end QAlgorithms.Papers.Independent.Intakethird100.P08

Source

On Cohomology theory for topological groups, arXiv:1009.4519v1, PDF p. 14, Lemma 2: domination by finitely many translates

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$ on whose square $\kappa$ is continuous. On $E=A\times G$ , define $(a,p)\star(b,q)=(a+\alpha_p(b)+\kappa(p,q),pq)$ , and use the topology generated by all sets $x\star(U_A\times U_G)$ , where $x\in E$ , $U_A$ is open and contains $0$ , $U_G$ is open and contains $1$ , and $\kappa$ is continuous on $U_G^2$ . For every pair of continuous functions $f,g:E\to\mathbb R$ whose sets of nonzero values have compact closures, assume $f(s)\ge0$ and $g(s)\ge0$ for every $s$ , and assume $g$ is not the zero function. Then there exist a natural number $n$ , coefficients $c_j>0$ , and points $u_j\in E$ , indexed by $j=0,\ldots,n-1$ , such that

f(s)\le\sum_{j=0}^{n-1}c_jg(u_j\star s)\quad\text{for every }s\in E.

The number $n$ need not be positive. When $n=0$ , coefficient positivity is vacuous and the conclusion is $f\le0$ , which under the assumptions means $f=0$ ; thus $f$ itself is allowed to be zero.

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