2 Haar Measure Foundation

2.1 Self-Duality on Compact Groups

Lemma 2.1 Haar Measure Preserved by Automorphisms

Let \(G\) be a compact second-countable topological group, \(\mu \) a Haar measure, and \(\phi : G \to G\) a bicontinuous group automorphism. Then \(\phi _*\mu = \mu \).

Proof ▶

Proved clean in HaarSelfDuality.lean (zero sorries, zero axioms). Uses MulEquiv.isHaarMeasure_map and mass preservation.

Theorem 2.2 Grassmannian Haar Self-Duality

✓

The shadow involution \(\phi : g \mapsto g^{-1}\) preserves the Haar measure on any compact group (instance: \(\mathrm{Gr}(2,4)\)).

Theorem 2.3 Adèlic Haar Self-Duality

✓

On any compact topological group, \(\phi _*\mu = \mu \) for \(\phi = (-)^{-1}\). Instance: \(\mathbb {A}^\times /\mathbb {Q}^\times \) with Haar measure \(d^\times a\) satisfies \(d^\times (a^{-1}) = d^\times a\).

Lemma 2.4 Compact Factor \(K^1 = \mathbb {A}^1/\mathbb {Q}^\times \)

The norm-\(1\) idèle class group \(K^1\) is compact (Fujisaki’s lemma, Weil 1974, Ch. IV §2).

Theorem 2.5 Peter-Weyl on \(K^1\)

\(L^2(K^1, d^\times a)\) decomposes into finite-dimensional irreducibles, so any left-invariant self-adjoint operator on \(L^2(K^1)\) has discrete spectrum.