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 covering ratios are finite and positive

Statement

For f0 and 0ϕ0 in Cc(G), (f:ϕ) is finite, is zero exactly when f=0, and is at least f/ϕ. Covering ratios are monotone in the first argument, positively homogeneous there (including scalar zero), subadditive, and exactly left invariant. For nonzero ϕ,ψ, (f:ψ)(f:ϕ)(ϕ:ψ). Consequently, for fixed nonzero f00 and nonzero f0, 0<1(f0:f)Iϕ(f)(f:f0)<.

Facts & Assumptions

Given: f,ϕ,ψ,f0 as stated.

[F1]

Ratios are infima of coefficient sums of finite translating covers. (Haar covering ratio of test functions)

[F3]

Compact sets admit finite subcovers; equivalently they satisfy the closed FIP condition. (A space is compact exactly when every family of closed subsets with the finite intersection property has nonempty intersection)

Proof

technique · direct
1.1

If f=0, the empty cover gives ratio zero. Otherwise put M=f>0. Choose y with ϕ(y)>0 and 0<t<ϕ(y). The open set W={ϕ>t} contains y. For every xsuppf, the translate xy1W contains x. Finitely many such translates cover the compact support, and coefficients M/t on them dominate f, so the infimum is finite.

F1F2F3
2.1

Every cover satisfies f(x)ϕcj for every x. Taking the supremum and then the infimum yields (f:ϕ)f/ϕ>0 when f0. In particular the normalizing denominator is finite and positive.

F1F2step 1.1
2.2

A cover of a larger function covers a smaller one. Multiplying coefficients by t>0 and dividing them back by t proves (tf:ϕ)=t(f:ϕ); scalar zero follows from the empty cover. Combining covers of f and g and taking independently arbitrarily close upper approximations to the two infima gives (f+g:ϕ)(f:ϕ)+(g:ϕ). Translating a cover by a replaces each centre xj by axj; translation by a1 reverses this operation. Thus (Laf:ϕ)=(f:ϕ).

F1step 1.1
3.1

If fjcjLxjϕ and ϕkdkLykψ, substitution gives fj,kcjdkLxjykψ. Choose the two coefficient sums below their finite infima plus δ>0 and let δ0. Their product proves the claimed composition inequality, also for f=0. Applying it to (f,f0,ϕ) gives the upper coordinate bound. Applying it to (f0,f,ϕ) and dividing the positive factors gives the lower bound.

F1step 1.1step 2.1

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

Used by

Dependency tree · two levels

29 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources