Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-12
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Haar integral comparison inequality

Statement

Assume AC and let I,J be nonzero positive left-invariant real Cc(G) functionals. For f≥0 and 0≠g≥0, I(f)≤(f:g)I(g). For real f∈Cc(G) and nonzero nonnegative symmetric u∈Cc(G), meaning u(z−1)=u(z), ∣I(f)J(u)−I(u)J(f)∣≤I(u)sup⁡z∈supp⁡uJ(∣Rzf−f∣). For every fixed f and ϵ>0, this supremum is <ϵ whenever supp⁡u lies in a sufficiently small identity neighbourhood. Such symmetric u exist, and I(u),J(u)>0.

Facts & Assumptions

Given: I,J,f,g,u as specified, with AC.

[F1]

Finite translating covers have finite coefficient-sum infima. (Haar covering ratios are finite and positive)

[F2]

Nonzero Haar integrals are strictly positive on nonzero nonnegative test functions. (Haar measure is positive on nonempty open sets and finite on compact sets)

[F3]

Translations are uniformly continuous in the parameter with a common compact support nearby. (Translations preserve compactly supported continuous functions)

[F4]

Continuous compact kernels admit commuting partial integrals under AC. (Compactly supported kernels admit commuting radon integrals)

[F5]

Under DC compactly supported cutoffs exist. (LCH Urysohn cutoff)

[F7]

AC covers the kernel and cutoff construction. (The Axiom of Choice)

Proof

technique · direct
1.1F1F6

For each cover f≤∑cjLxjg, positivity and left invariance give I(f)≤∑cjI(g). Taking the infimum gives I(f)≤(f:g)I(g), including f=0.

1.2F3F4F7

Write K=supp⁡f, S=supp⁡u. The continuous kernel f(x)u(x−1y) has support in the compact set K×KS; compactness here follows from compact products and continuous multiplication as in [F3]. Integrating y by left invariance yields I(f)J(u). Interchanging integrals and substituting x=yz by left invariance of I yields JyIzf(yz)u(z−1)=JyIzf(yz)u(z). The transformed kernel is supported in KS−1×S, so a second application of [F4] gives I(f)J(u)=Izu(z)Jyf(yz).

2.1F3F4F5F6step 1.2

Subtract I(u)J(f). For every z, ∣J(Rzf−f)∣≤J(∣Rzf−f∣) by positivity. The latter is continuous in z: [F3] and ∣∣h∣−∣k∣∣≤∣h−k∣, dominated on a common compact support by a cutoff, give the same continuity bound as in [F4]. Hence its supremum on compact S is finite. Positivity applied to u times this bound proves the stated comparison inequality.

3.1F2F3F5F6F7∎

On a compact identity neighbourhood, all Rzf−f have support in one compact set C. Choose a cutoff c=1 on C. Then J(∣Rzf−f∣)≤∥Rzf−f∥∞J(c)→0. If J(c)=0 the bound is already zero. Given ϵ, choose a neighbourhood with this bound <ϵ/2, ensuring the supremum is at most ϵ/2<ϵ. Inside a smaller symmetric open neighbourhood W, take 0≤v≤1W with v(e)=1, and set w=(2v−1)+ and u(z)=w(z)w(z−1). Its support is contained in W, it is symmetric, and u(e)=1. Strict positivity gives I(u),J(u)>0.

Sources

Pedersen, Haar integral, p.2 definitions and lemma; p.3 Theorem 1; pp.4–5 second proof and Remark 2. Local argument and conventions as displayed above.

Depends on

Dependency tree · 2 levels

Sources