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 and in , is finite, is zero exactly when , and is at least . Covering ratios are monotone in the first argument, positively homogeneous there (including scalar zero), subadditive, and exactly left invariant. For nonzero , Consequently, for fixed nonzero and nonzero ,
Facts & Assumptions
Given: as stated.
Ratios are infima of coefficient sums of finite translating covers. (Haar covering ratio of test functions)
Continuous functions on a nonempty compact support have bounded absolute value and attain a maximum. (A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism)
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
If , the empty cover gives ratio zero. Otherwise put . Choose with and . The open set contains . For every , the translate contains . Finitely many such translates cover the compact support, and coefficients on them dominate , so the infimum is finite.
Every cover satisfies for every . Taking the supremum and then the infimum yields when . In particular the normalizing denominator is finite and positive.
A cover of a larger function covers a smaller one. Multiplying coefficients by and dividing them back by proves ; scalar zero follows from the empty cover. Combining covers of and and taking independently arbitrarily close upper approximations to the two infima gives . Translating a cover by replaces each centre by ; translation by reverses this operation. Thus .
If and , substitution gives . Choose the two coefficient sums below their finite infima plus and let . Their product proves the claimed composition inequality, also for . Applying it to gives the upper coordinate bound. Applying it to and dividing the positive factors gives the lower bound.
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
- Haar covering ratio of test functions
- A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism
- A space is compact exactly when every family of closed subsets with the finite intersection property has nonempty intersection
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
- Pedersen, Haar integral, p.2 definitions and lemma; p.3 Theorem 1; pp.4–5 second proof and Remark 2 (standard reference, not scraped)