Existence of a nonzero positive left-invariant integral
OpenQAlgorithms.Papers.Independent.Intakethird100.P08.proposition5Let be a Hausdorff locally compact second-countable topological group and let be a Hausdorff locally compact second-countable abelian topological group with a continuous action of by automorphisms, written . Let be a Borel measurable two-cocycle, with pointwise identity
Assume that is continuous on , where is an open identity neighborhood. Let , with multiplication and inverse . Equip with the topology generated by left translates of the rectangles , where are open identity neighborhoods and is continuous on . Write and .
Let be the real vector space of continuous compactly supported real functions. There exists a real linear functional such that
where again belongs to . This positive integral is the real form of the integral whose complexification is used by the source.
import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P08
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]
/-- Proposition 5, PDF p. 17: existence of a nonzero positive invariant
integral on the actual test-function space. Its complex-linear extension is
the usual complexification of this real positive integral. -/
theorem proposition5 (D : LocalCocycle G A) :
∃ I : C_c(ExtensionPoint D, ℝ) →ₗ[ℝ] ℝ,
IsPositiveInvariantIntegral D I := by sorry
end ConstructedExtension
end QAlgorithms.Papers.Independent.Intakethird100.P08
Read-back
What the Lean code literally says, in plain math · gpt-6.1-sol
Let be a Hausdorff, locally compact, second countable topological group, and let be a Hausdorff, locally compact, second countable additive abelian topological group, both with their Borel measurable structures. For every datum consisting of additive automorphisms satisfying , , and continuity of ; a measurable function satisfying and ; and an open neighborhood of such that is continuous on , put and define . Give the topology generated by all sets , where , is open and contains , is open and contains , and is continuous on . Then there exists a real-linear map , where consists of continuous real functions whose nonzero sets have compact closures, such that , for every everywhere nonnegative , and for every and every , there exists satisfying for every and .
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.