Strictly positive integral and its locally finite Borel measure

Open

QAlgorithms.Papers.Independent.Intakethird100.P08.remark4

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 $I:C_c(E;\mathbb R)\to\mathbb R$ be any nonzero positive real linear left-invariant integral as in Proposition 5. It is strictly positive on every nonzero nonnegative test. Moreover it has a nonzero representing Borel measure $\mu$ such that

\begin{gathered} 0\ne f\ge0\Longrightarrow I(f)>0,\qquad I(f)=\int_E f\,d\mu\quad(f\in C_c(E;\mathbb R)),\\ \mu(xW)=\mu(W)\quad(x\in E,\ W\text{ Borel},\ \overline W\text{ compact}),\\ \mu(K)<\infty\quad(K\subseteq E\text{ compact}). \end{gathered}

Every displayed test function is integrable for $\mu$ . The measure is the Riesz representative of the integral.

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]

/-- Remark 4, PDF p. 17: strict positivity and the representing locally
finite left-invariant Borel measure. Printed x in G is corrected to x in E,
as already specified by Proposition 5(ii). Integrability is explicit. -/
theorem remark4 (D : LocalCocycle G A)
    (I : C_c(ExtensionPoint D, ℝ) →ₗ[ℝ] ℝ)
    (hI : IsPositiveInvariantIntegral D I) :
    (∀ f : C_c(ExtensionPoint D, ℝ), (∀ s, 0 ≤ f s) → f ≠ 0 → 0 < I f) ∧
    ∃ mu : Measure (ExtensionPoint D), IsLeftInvariantMeasure D mu ∧
      ∀ f : C_c(ExtensionPoint D, ℝ), Integrable f mu ∧
        (∫ s, f s ∂mu) = I f := by sorry

end ConstructedExtension

end QAlgorithms.Papers.Independent.Intakethird100.P08

Source

On Cohomology theory for topological groups, arXiv:1009.4519v1, PDF p. 17, Remark 4: left-invariant locally finite Borel measure

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:A\to A$ satisfying $\rho_1=\mathrm{id}$ and $\rho_{gh}=\rho_g\circ\rho_h$ , with $(g,a)\mapsto\rho_g(a)$ jointly continuous; 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$ such that $c$ is continuous on $N\times N$ . On the set $E=A\times G$ , write $(a,g)\star(b,h)=(a+\rho_g(b)+c(g,h),gh)$ . Equip $E$ with the topology generated by all sets $\{x\star(a,g):a\in P,\ g\in Q\}$ , where $x\in E$ , $P\subseteq A$ is open and contains $0$ , $Q\subseteq G$ is open and contains $1$ , and $c$ is continuous on $Q\times Q$ ; equip $E$ with the Borel measurable structure of this topology. Let $C_c(E,\mathbb R)$ denote the continuous real functions with compact support. Suppose $I:C_c(E,\mathbb R)\to\mathbb R$ is a nonzero real-linear map, $I(f)\ge0$ whenever $f$ is pointwise nonnegative, and, for every $f\in C_c(E,\mathbb R)$ and $x\in E$ , there exists $f_x\in C_c(E,\mathbb R)$ satisfying $f_x(s)=f(x\star s)$ for every $s$ and $I(f_x)=I(f)$ . Then $I(f)>0$ for every pointwise nonnegative $f\in C_c(E,\mathbb R)$ that is not the zero function. Moreover, there exists a nonzero Borel measure $\mu$ 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\subseteq E$ whose closure is compact, and every $f\in C_c(E,\mathbb R)$ is $\mu$ -integrable with $\int_E f(s)\,d\mu(s)=I(f)$ .

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