Initial definitions
Scaling Haar measure on a group
Let \(A\) be a locally compact topological additive abelian group. There's then a regular additive Haar measure \(\mu\) on \(A\), unique up to a positive scalar factor. If \(\phi:(A,+)\cong(A,+)\) is a homeomorphism and an additive automorphism of \(A\), then we can push forward \(\mu\) along \(\phi\) to get a second measure \(\phi_*\mu\) on \(A\), with the property that \((\phi_*\mu)(X)=\mu(\phi^{-1}X)\) for any Borel subset \(X\) of \(A\).
Now \(\phi_*\mu\) is a translation-invariant and regular measure, and hence also a Haar measure on \(A.\) It must thus differ from \(\mu\) by a positive scalar factor, which we call \(d_A(\phi)\). There is a choice of normalization here between \(d_A(\phi)\) and \(d_A(\phi)^{-1}\), so let us be more precise.
DefinitionMeasureTheory.addEquivAddHaarChar#
If \(A\) is a locally compact topological additive abelian group, if \(\mu\) is a regular Haar measure on \(A\), and if \(\phi:A\to A\) is an additive homeomorphism, then we let \(d_A(\phi)\) denote the unique positive real number such that \(\mu(X)=d_A(\phi)(\phi_*\mu)(X)\) for any Borel set \(X\).
Used by 7
To give an example, if \(\phi\) is multiplication by \(2\) on the real numbers, if \(X=[0,1]\), and if \(\mu\) is Lebesgue measure on the Borel subsets of \(\mathbb{R}\), we have that \(\phi_*\mu(X)=\mu(\phi^{-1}(X))=\mu([0,1/2])=1/2\), so \(1=d_A(\phi)/2\) meaning that \(d_A(\phi)=2\). Similarly if \(\phi\) is multiplication by \(-2\) and \(X=[0,1]\) then \(\phi^{-1}(X)=[-1/2,0]\) which again has measure \(1/2\), so \(d_A(\phi)\) is 2 again.
Strictly speaking our definition of \(d_A(\phi)\) depends on the choice of regular Haar measure \(\mu\). Note that mathlib offers a fixed Borel regular Haar measure MeasureTheory.Measure.haar on any locally compact topological group and the actual definition of \(d_A\) in the code uses this definition. Note also that the code defines everything for multiplicative groups and uses @[to_additive] to deduce the corresponding results for additive groups.
Here are some basic results about this construction. In all of them, \(A\) is a locally compact topological group and \(\phi:A\to A\) is a group isomorphism and a homeomorphism. The first lemma shows that the definition of \(d_A(\phi)\) is indeed independent of the choice of Haar measure.
LemmaMeasureTheory.addEquivAddHaarChar_eq#
\(d_A(\phi)\) is independent of choice of regular Haar measure.
Proof
If \(\mu'\) is a second choice then \(\mu'=\lambda\mu\) for some positive real \(\lambda\), and the \(\lambda\)s on each side of \(\mu'(X)=d_A(\phi)(\phi_*\mu')(X)\) cancel.
Lean
Formalized as MeasureTheory.addEquivAddHaarChar_eq.
Sources
Uses 1 · Used by 2
LemmaMeasureTheory.addEquivAddHaarChar_smul_map#
If \(\mu\) is any regular Haar measure on \(A\) then \(d_A(\phi)(\phi_*\mu) = \mu.\)
Proof
This is a restatement of the previous result.
Lean
Formalized as MeasureTheory.addEquivAddHaarChar_smul_map.
Sources
Uses 1 · Used by 3
We can of course also pull a Haar measure \(\mu\) back along a homeomorphism \(\phi\), giving a measure \(\phi^*\mu\) such that \(\phi^*\mu(X)=\mu(\phi(X))\).
CorollaryMeasureTheory.addEquivAddHaarChar_comap#
If \(\mu\) is any regular Haar measure on \(A\) then \(d_A(\phi)\mu = \phi^*\mu.\)
Proof
This follows from lemma MeasureTheory.addEquivAddHaarChar_smul_map applied to the regular Haar measure \(\phi^*\mu\) and the fact that \(\phi_*\phi^*\mu=\mu\).
Lean
Formalized as MeasureTheory.addEquivAddHaarChar_smul_eq_comap.
Sources
Uses 1 · Used by 1
Now let \(\mu\) be any regular additive Haar measure on \(A\).
LemmaMeasureTheory.addEquivAddHaarChar_smul_preimage#
If \(X\) is a Borel set then \(\mu(X)=d_A(\phi)\mu(\phi^{-1}X)\).
Proof
This follows immediately from lemma MeasureTheory.addEquivAddHaarChar_smul_map and the definition of the pushforward of a measure.
Lean
Formalized as MeasureTheory.addEquivAddHaarChar_smul_preimage.
Sources
Uses 2 · Used by 2
LemmaMeasureTheory.addEquivAddHaarChar_smul_integral_map#
If \(f:A\to\mathbb{R}\) is a Borel measurable function then \(d_A(\phi)\int f(x)d\phi_*\mu(x)=\int f(x)d\mu(x)\).
Proof
This also follows immediately from lemma MeasureTheory.addEquivAddHaarChar_smul_map.
Lean
Formalized as MeasureTheory.addEquivAddHaarChar_smul_integral_map.
Sources
Uses 2 · Used by 1
We also have the following variant:
LemmaMeasureTheory.addEquivAddHaarChar_smul_integral_comap#
If \(f:A\to\mathbb{R}\) is a Borel measurable function then \(d_A(\phi)\int f(x)d\mu(x)=\int f(x)d\phi^*\mu(x)\).
Proof
This is immediate from corollary MeasureTheory.addEquivAddHaarChar_comap.
Lean
Formalized as MeasureTheory.integral_comap_eq_addEquivAddHaarChar_smul.
Sources
Uses 1 · Used by 1
Note that as a consequence of lemma MeasureTheory.addEquivAddHaarChar_smul_preimage, if \(X\) is a Borel subset of \(A\) with positive finite measure then we can read off \(d_A(\phi)\) by \(d_A(\phi)=\mu(X)/\mu(\phi^{-1}(X))\), and hence also by \(d_A(\phi)=\mu(\phi(X))/\mu(X)\). A nice special case is when \(\mu(X)=1\), in which case we have \(d_A(\phi)=\mu(\phi(X))\) for all \(\phi\), or \(d_A(\phi)=1/\mu(\phi^{-1}(X))\). Similarly, by lemma MeasureTheory.addEquivAddHaarChar_smul_integral_map, if \(f\) is a measurable function with \(0\lt \int f(x)d\mu(x)\lt \infty\) then we can read off \(d_A(\phi)\) by \(d_A(\phi)=(\int f(x)d\mu(x))/(\int f(x)\phi_*\mu(x))\). Note that mathlib supplies such \(f\) with the function exists_continuous_nonneg_pos. The following are also straightforward.
LemmaMeasureTheory.addEquivAddHaarChar_refl#
\(d_A(id)=1.\)
Uses 2 · Used by 1
LemmaMeasureTheory.addEquivAddHaarChar_trans#
\(d_A(\phi\circ\psi)=d_A(\phi)d_A(\psi).\)
Proof
Here's one way: it suffices to prove that \(d_A(\phi\circ\psi)(\phi\circ\psi)_*\mu=d_A(\phi)d_A(\psi)(\phi\circ\psi)_*\mu\) (because there exists a compact set with positive finite measure) and using lemma MeasureTheory.addEquivAddHaarChar_smul_map and the fact that \((\phi\circ\psi)_*\mu=\phi_*(\psi_*\mu)\) one can simplify both sides to \(\mu\).
Lean
Formalized as MeasureTheory.addEquivAddHaarChar_trans.
Sources
Uses 2 · Used by 1
Scaling Haar measure on a ring
Now let \(R\) be a locally compact topological ring. The Haar character of \(R\), or more precisely the left Haar character of \(R\), is a group homomorphism \(R^\times\to\mathbb{R}^\times\) defined in the following way. If \(u\in R^\times\) then left multiplication by \(u\), namely the map \(\ell_u:(R,+)\to(R,+)\) defined by \(\ell_u(r)=ur\), is a homeomorphism and an additive automorphism of \((R,+)\), so the preceding theory applies to \(\ell_u\).
DefinitionMeasureTheory.ringHaarChar#
We define \(\delta_R(u)\) (or just \(\delta(u)\) when the ring \(R\) is clear) to be \(d_R(\ell_u)\).
Uses 3 · Used by 4
Lemmas MeasureTheory.addEquivAddHaarChar_refl and MeasureTheory.addEquivAddHaarChar_trans immediately imply that \(\delta_R\) is a group homomorphism from \(R^\times\) to \(\mathbb{R}_{>0}\). Also immediate from previous lemmas is
LemmaMeasureTheory.ringHaarChar_mul_integral#
If \(f:R\to\mathbb{R}\) is a Borel measurable function and \(u\in R^\times\) then \(\delta_R(u)\int f(ux)d\mu(x)=\int f(x)d\mu(x)\).
Proof
A short calculation using lemma MeasureTheory.addEquivAddHaarChar_smul_integral_map.
Lean
Formalized as MeasureTheory.ringHaarChar_mul_integral.
Sources
Uses 2 · Used by 1
LemmaMeasureTheory.ringHaarChar_mul_volume#
If \(X\) is a Borel subset of \(R\) and \(r\in R^\times\) then \(\mu(rX)=\delta_R(r)\mu(X)\).
Proof
Immediate from lemma MeasureTheory.addEquivAddHaarChar_smul_preimage.
Lean
Formalized as MeasureTheory.ringHaarChar_mul_volume.
Sources
Uses 2 · Used by 3
The next result lies a little deeper.
CorollaryMeasureTheory.ringHaarChar_continuous#
The function \(\delta_R:R^\times\to\mathbb{R}_{>0}\) is continuous.
Proof
Fix a Haar measure \(\mu\) on \(R\) and a continuous real-valued function \(f\) on \(R\) with compact support and such that \(\int f(x) d\mu(x)\not=0\). Then \(r \mapsto \int f(rx) d\mu(x)\) is a continuous function from \(R\to\mathbb{R}\) (because a continuous function with compact support is uniformly continuous) and thus gives a continuous function \(R^\times\to\mathbb{R}\). Thus the function \(u\mapsto (\int f(ux) d\mu(x))/(\int f(x)d\mu(x))\) is a continuous function from \(R^\times\) to \(\mathbb{R}\) taking values in \(\mathbb{R}_{>0}\). Hence \(\delta_R^{-1}\) is continuous, from lemma MeasureTheory.ringHaarChar_mul_integral, and thus \(\delta_R\) is too.
Lean
Formalized as MeasureTheory.ringHaarChar_continuous.
Sources
Uses 2 · Used by 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.