Near additivity with support uniformly near identity

Open

QAlgorithms.Papers.Independent.Intakethird100.P08.lemma5

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

For $f,h\in C_c^+(E)$ with $h\ne0$ , let $(f;h)$ be the infimum of $\sum_{j=1}^r c_j$ over finite covers $f(s)\le\sum_{j=1}^r c_jh(u_js)$ for every $s\in E$ , with $c_j\ge0$ and $u_j\in E$ . For fixed $0\ne g\in C_c^+(E)$ and $0\ne\varphi\in C_c^+(E)$ , define $I_\varphi(f)=(f;\varphi)/(g;\varphi)$ .

Given $f_1,f_2\in C_c^+(E)$ and $\varepsilon>0$ , there exists a neighborhood $V$ of $e$ , chosen before $\varphi$ , such that

0\ne\varphi\in C_c^+(E),\quad\operatorname{supp}\varphi\subseteq V \quad\Longrightarrow\quad \big|I_\varphi(f_1)+I_\varphi(f_2)-I_\varphi(f_1+f_2)\big|\le\varepsilon.

Thus the additivity defect is uniformly small for all sufficiently localized tests.

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 5, PDF pp. 15--17: the neighborhood is uniform over every eligible
phi. The absolute-value headline is retained; the erroneous intermediate p. 16
line is not used (its intended estimate is printed on p. 17). -/
theorem lemma5 (D : LocalCocycle G A) (g f1 f2 : ExtensionPoint D → ℝ)
    (hg : IsNonnegativeTest D g) (hg0 : g ≠ 0)
    (hf1 : IsNonnegativeTest D f1) (hf2 : IsNonnegativeTest D f2)
    (eps : ℝ) (heps : 0 < eps) :
    ∃ V : Set (ExtensionPoint D), V ∈ nhds (identityPoint D) ∧
      ∀ phi : ExtensionPoint D → ℝ, IsNonnegativeTest D phi → phi ≠ 0 →
        tsupport phi ⊆ V →
        |normalizedIntegral D g phi f1 + normalizedIntegral D g phi f2 -
          normalizedIntegral D g phi (f1 + f2)| ≤ 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 5: near additivity

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$ consist of 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. Put $E=A\times G$ , define $(a,p)\star(b,q)=(a+\alpha_p(b)+\kappa(p,q),pq)$ , and equip $E$ with the topology generated by $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 functions $h,k:E\to\mathbb R$ , let $C(h,k)$ be the real infimum of the sums $\sum_{j=0}^{n-1}c_j$ over finite families $c_j\ge0$ , $u_j\in E$ , satisfying $h(s)\le\sum_{j=0}^{n-1}c_jk(u_j\star s)$ for every $s$ ; $n=0$ is allowed, empty sums are $0$ , and the infimum of an empty cost set is $0$ . Set $J_{g,\phi}(h)=C(h,\phi)/C(g,\phi)$ , with division by zero giving $0$ . For every three continuous, everywhere nonnegative functions $g,f_1,f_2:E\to\mathbb R$ , each with compact closure of its nonzero set, assume $g\ne0$ . For every $\varepsilon>0$ , there exists a neighborhood $V$ of $(0,1)$ such that every continuous, everywhere nonnegative, nonzero function $\phi:E\to\mathbb R$ with compact closure of its nonzero set and with $\overline{\{s:\phi(s)\ne0\}}\subseteq V$ satisfies

\left|J_{g,\phi}(f_1)+J_{g,\phi}(f_2)-J_{g,\phi}(f_1+f_2)\right| \le\varepsilon.

The neighborhood $V$ need not itself be open, and $f_1$ and $f_2$ may be zero. The conclusion does not separately assert the existence of any $\phi$ satisfying the conditions for the chosen $V$ .

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