LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-02

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.

Composition of Weil quotient integrals

Statement

Assume AC. For closed $L \leq H \leq G$ and rho-functions $ρ_{G L}, ρ_{G H}, ρ_{H L}$ with their Weil measures, define $r_{x} (h L) = \frac{ρ_{G L} (x h)}{ρ_{G H} (x h) ρ_{H L} (h)} .$ Then $r_{x}$ is positive continuous on $H / L$ , and for $ϕ \in C_{c} (G / L)$ , $\int_{G / L} ϕ (q) d μ_{G L} (q) = \int_{G / H} \int_{H / L} ϕ (x h L) r_{x} (h L) d μ_{H L} (h L) d μ_{G H} (x H) .$ The inner integral is independent of the chosen representative $x$ .

Facts & Assumptions

Given: AC, closed $L \leq H \leq G$ , fixed compatible left Haar measures, rho-functions and Weil measures.

[F1]

The rho covariance law for each subgroup pair (Rho-function for a closed subgroup).

[F2]

The Weil formula for $G / L$ , $G / H$ , and $H / L$ (Weil formula with a rho-function).

[F3]

$T_{L} : C_{c} (G) \to C_{c} (G / L)$ is onto (Compact lifts and averaging onto C_c(G/H)).

[F4]

Compactly supported continuous kernels have continuous compactly supported partial integrals, and the associated positive Radon integrations commute (Compactly supported kernels admit commuting radon integrals).

[A1]

AC is the choice-function principle required by the stated hypothesis (The Axiom of Choice).

Proof

technique · direct

1.1F1construct

Under $h \mapsto h l$ , the numerator of $r_{x}$ is multiplied by $Δ_{L} (l) Δ_{G} (l)^{- 1}$ ; the two denominator factors multiply together by the same amount. Thus $r_{x} (h l) = r_{x} (h)$ . Its positive continuous lift on $H$ therefore descends continuously to $H / L$ .

1.2F1F2construct

Fix $x \in G$ and put $u_{x} (h) = f (x h) ρ_{G L} (x h) / (ρ_{G H} (x h) ρ_{H L} (h))$ for $f \in C_{c} (G)$ . The support in $H$ is compact. By [F1], this function is constant under right $L$ in its rho ratio, and $u_{x} (h l) = f (x h l) r_{x} (h L)$ . The $H / L$ Weil formula gives $\int_{H / L} T_{L} f (x h L) r_{x} (h L) d μ_{H L} (h L) = \int_{H} u_{x} (h) ρ_{H L} (h) d h = \int_{H} f (x h) \frac{ρ_{G L} (x h)}{ρ_{G H} (x h)} d h .$ All integrals are finite by compact support.

2.1step 1.2algebra

The final expression in step 1.2 is unchanged when $x$ is replaced by $x k$ for $k \in H$ : substitute $j = k h$ and use left invariance of Haar measure on $H$ . Hence it descends to a function of $x H$ .

3.1A1F2F3F4step 1.1step 1.2step 2.1

Integrate step 1.2 over $G / H$ . Set $v (x) = f (x) ρ_{G L} (x) / ρ_{G H} (x) \in C_{c} (G)$ . The inner expression in step 1.2 is $T_{H} v (x H)$ ; local compact support and [F4] make this a continuous compactly supported quotient function. Applying the $G / H$ Weil formula to $v$ shows that the iterated integral is $\int_{G} f (x) ρ_{G L} (x) d x$ . Applying the $G / L$ Weil formula to $f$ gives the same value as $\int_{G / L} T_{L} f d μ_{G L}$ . Thus the asserted identity holds for $ϕ = T_{L} f$ ; surjectivity [F3] proves it for every $C_{c} (G / L)$ test function. ∎

Sources

Bekka–de la Harpe–Valette, Kazhdan’s Property (T), Appendix E §E.2, proof route preceding Theorem E.2.4, PDF pp. 416–419. The source’s induction-in-stages argument is a sketch; this quotient-integral composition is written out here.

Depends on

Used by

Induction in stages for closed subgroup chains Theorem

Dependency tree · two levels

17 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

Bekka–de la Harpe–Valette, Kazhdan’s Property (T), Appendices B and E (standard reference, not scraped)
Bruhat, Lectures on Lie Groups and Representations of Locally Compact Groups, Chapters 1 and 7 (standard reference, not scraped)
David Vogan, Unitary Representations of Locally Compact Groups and Induced Representations (standard reference, not scraped)