Four normalized approximate-integral inequalities

Open

QAlgorithms.Papers.Independent.Intakethird100.P08.lemma3

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

For $f,f_1,f_2\in C_c^+(E)$ one has

\begin{gathered} f\ne0\Longrightarrow (g;f)^{-1}\le I_\varphi(f)\le(f;g),\\ I_\varphi(f_x)=I_\varphi(f)\quad(x\in E),\\ I_\varphi(f_1+f_2)\le I_\varphi(f_1)+I_\varphi(f_2),\\ I_\varphi(cf)=cI_\varphi(f)\quad(c\ge0). \end{gathered}

These bounds and covariance properties describe the normalized approximate integrals on the nonnegative cone.

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 3(i)--(iv), PDF pp. 14--15. Printed x in G is corrected to x in E,
as required by f_x and the proof on p. 17(ii). The omitted g≠0 is retained
from that proof and is necessary to normalize the denominator. -/
theorem lemma3 (D : LocalCocycle G A)
    (g phi f f1 f2 : ExtensionPoint D → ℝ)
    (hg : IsNonnegativeTest D g) (hg0 : g ≠ 0)
    (hphi : IsNonnegativeTest D phi) (hphi0 : phi ≠ 0)
    (hf : IsNonnegativeTest D f) (hf1 : IsNonnegativeTest D f1)
    (hf2 : IsNonnegativeTest D f2) :
    (f ≠ 0 → (approximateIntegral D g f)⁻¹ ≤ normalizedIntegral D g phi f ∧
      normalizedIntegral D g phi f ≤ approximateIntegral D f g) ∧
    (∀ x : ExtensionPoint D,
      normalizedIntegral D g phi (leftTranslate D f x) = normalizedIntegral D g phi f) ∧
    (normalizedIntegral D g phi (f1 + f2) ≤
      normalizedIntegral D g phi f1 + normalizedIntegral D g phi f2) ∧
    (∀ c : ℝ, 0 ≤ c → normalizedIntegral D g phi (c • f) =
      c * normalizedIntegral D g phi f) := by sorry

end ConstructedExtension

end QAlgorithms.Papers.Independent.Intakethird100.P08

Source

On Cohomology theory for topological groups, arXiv:1009.4519v1, PDF p. 14, Lemma 3: normalized approximate-integral inequalities

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$ , with $(a,p)\star(b,q)=(a+\alpha_p(b)+\kappa(p,q),pq)$ , and equip it with the topology generated by $x\star(U_A\times U_G)$ for $x\in E$ , open $U_A\ni0$ , and open $U_G\ni1$ such that $\kappa$ is continuous on $U_G^2$ . For functions $h,k:E\to\mathbb R$ , define $C(h,k)$ as the real infimum of all costs $\sum_{j=0}^{n-1}c_j$ with $n\ge0$ , $c_j\ge0$ , $u_j\in E$ , and $h(s)\le\sum_{j=0}^{n-1}c_jk(u_j\star s)$ for every $s$ ; empty sums are $0$ , and an empty cost set has infimum $0$ . Define $J_{g,\phi}(h)=C(h,\phi)/C(g,\phi)$ and $L_xh(s)=h(x\star s)$ . For every five functions $g,\phi,f,f_1,f_2:E\to\mathbb R$ , assume each is continuous, everywhere nonnegative, and has compact closure of its nonzero set; also assume $g\ne0$ and $\phi\ne0$ . Then all four assertions hold:

\begin{gathered} f\ne0\ \Longrightarrow\ C(g,f)^{-1}\le J_{g,\phi}(f)\le C(f,g),\\ J_{g,\phi}(L_xf)=J_{g,\phi}(f)\qquad(x\in E),\\ J_{g,\phi}(f_1+f_2)\le J_{g,\phi}(f_1)+J_{g,\phi}(f_2),\\ J_{g,\phi}(cf)=c\,J_{g,\phi}(f)\qquad(c\in\mathbb R,\ c\ge0). \end{gathered}

Addition and scalar multiplication of functions are pointwise. The functions $f,f_1,f_2$ may be zero; the condition $f\ne0$ applies only to the first pair of bounds. Real inversion and division use the conventions $0^{-1}=0$ and $a/0=0$ .

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