ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-08

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.

A square-integrable discrete-series matrix coefficient

Example

For $D_{2}^{-}$ , let $u_{2}$ be the normalized extremal K-vector from Matrix-coefficient formulas and decay for the discrete and principal series. Its coefficient $c_{2} (g) = ⟨ π_{2} (g) u_{2}, u_{2} ⟩$ satisfies $c_{2} (a_{τ}) = {sech}^{2} (τ / 2)$ and has exact squared norm $\int_{G} ∣ c_{2} (g) ∣^{2} d g = 4 π$ for the fixed left Haar measure. The assigned theorem Square integrability of discrete-series matrix coefficients supplies the broader K-finite coefficient result for $D_{2}^{-}$ . At the $n = 1$ limit endpoint, the compact-picture weight-one coefficient $c_{1} (a_{τ}) = sech (τ / 2)$ instead has infinite squared integral.

Facts & Assumptions

Given: AC, the holomorphic discrete-series model $D_{2}^{-}$ , the compact-picture weight-one endpoint, and the fixed left Haar measure on $G = {S L}_{2} (R)$ .

[F1]

The normalized extremal vector $u_{2}$ is K-finite in the strongly continuous unitary model $D_{2}^{-}$ and has coefficient $c_{2} (a_{τ}) = \cosh (τ / 2)^{- 2}$ (Matrix-coefficient formulas and decay for the discrete and principal series(a), Square integrability of discrete-series matrix coefficients).

[F2]

Matrix coefficients use the first-variable-linear pairing; the coefficient of a strongly continuous unitary representation is continuous (Matrix coefficient of a unitary representation).

[F3]

If $∣ c ∣$ is continuous and $K$ -bi-invariant, then $\int_{G} ∣ c (g) ∣^{2} d g = 2 π \int_{0}^{\infty} ∣ c (a_{τ}) ∣^{2} \sinh τ d τ$ for the fixed Haar measure (Left Haar integral and left Haar measure, KAK integration formula for K-bi-invariant functions on SL2(R)).

[F4]

Every matrix coefficient of K-finite vectors in $D_{2}^{-}$ lies in $L^{2} (G)$ , and $D_{2}^{-}$ embeds as a closed invariant subspace of the left regular representation (Square integrability of discrete-series matrix coefficients).

[F5]

In the strongly continuous unitary odd compact picture at the endpoint, $c_{1} (a_{τ}) = sech (τ / 2)$ for the unit weight-one vector (Matrix-coefficient formulas and decay for the discrete and principal series(b)).

[F6]

For a nonnegative measurable function $h$ , if $h_{m} ↑ h$ pointwise, then $\int h_{m} d μ ↑ \int h d μ$ (Monotone convergence for the integral).

[A1]

AC is assumed and inherited through the normalized discrete-series and fixed-Haar constructions (The Axiom of Choice).

Verification

technique · direct

Given: The vectors, representations, Haar measure and facts above.

1.1F1F2

Let $c_{2} (g) = ⟨ π_{2} (g) u_{2}, u_{2} ⟩$ . By [F1], $c_{2} (a_{τ}) = {sech}^{2} (τ / 2)$ . The vector $u_{2}$ is a $K$ -eigenvector, so unitarity gives $c_{2} (k_{1} g k_{2}) = χ (k_{1}) χ (k_{2}) c_{2} (g)$ for its character $χ$ ; hence $∣ c_{2} ∣^{2}$ is continuous and $K$ -bi-invariant by [F2].

2.1F3F6step 1.1algebraA1

Applying [F3] gives $\int_{G} ∣ c_{2} (g) ∣^{2} d g = 2 π \int_{0}^{\infty} {sech}^{4} (τ / 2) \sinh τ d τ$ . Set $u = τ / 2$ ; the radial integrand times $d τ$ becomes $4 \sinh u \cosh^{- 3} u d u$ . For $M > 0$ , its integral on $[0, M]$ is $2 (1 - \cosh^{- 2} M)$ , which tends to $2$ . The truncated integrands increase to the full nonnegative integrand, so [F6] gives the full radial integral $2$ and therefore $∥ c_{2} ∥_{2}^{2} = 4 π$ .

3.1F3F4F5F6step 2.1algebra∎

By [F4], this explicit coefficient lies within the K-finite square-integrable coefficient family of $D_{2}^{-}$ . At the $n = 1$ endpoint, [F5] and [F3] instead give $\int_{G} ∣ c_{1} (g) ∣^{2} d g = 2 π \int_{0}^{\infty} 2 \tanh (τ / 2) d τ = + \infty$ : for $τ \geq \log 3$ the integrand is at least $1$ , and $1_{[\log 3, \log 3 + m]} ↑ 1_{[\log 3, \infty)}$ has integral $m$ , so [F6] forces divergence. Thus the concrete $n = 2$ coefficient is square-integrable while the displayed limit coefficient is not.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

44 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

Emmanuel Kowalski, An Introduction to the Representation Theory of Groups (AMS GSM 155; author's PDF) (standard reference, not scraped)
Peter Hochs, Harish-Chandra's Plancherel formula for SL(2,R) (lecture notes) (standard reference, not scraped)