Finite Products
Here are two facts which we will need about products.
LemmaMeasureTheory.addEquivAddHaarChar_prodCongr#
If \((A,+)\) and \((B,+)\) are locally compact topological abelian groups, and if \(\phi:A\to A\) and \(\psi:B\to B\) are additive homeomorphisms, then \(\phi\times\psi:A\times B\to A\times B\) is an additive homeomorphism (this is obvious), and \(d_{A\times B}(\phi\times\psi)=d_A(\phi)d_B(\psi)\).
Proof
We only need this result in the case where both \(A\) and \(B\) are second-countable, in which case Prod.borelSpace can be used to show that Haar measure on \(A\times B\) is the product of Haar measures on \(A\) and \(B\), and in this case the result follows easily. Without this assumption, the product of these measures may not even be a Borel measure and one has to be more careful. The proof in this case is explained by Gouëzel here. Here is the idea. Let \(\rho\) be a Haar measure on \(A\times B\). Fix sets \(X\subseteq A\) and \(Y\subseteq B\) which are compact with nonempty interior. We can now pull back \(\rho\) to a measure \(\nu\) on the Borel sigma-algebra of \(A\) defined as \(\nu(s)=\rho(s\times Y)\) and this is easily checked to be a Haar measure on \(A\). Then \(\delta_{A\times B}(a,0)\nu(X)= \delta_{A\times B}(a,0)\rho(X\times Y)=\rho((a,0)(X\times Y))= \rho(aX\times Y)=\nu(aX)=\delta_A(a)\nu(X)\) , so \(\delta_{A\times B}(a,0)=\delta_A(a)\). Similarly \(\delta_{A\times B}(0,b)=\delta_B(b)\) and because \(\delta_{A\times B}\) is a group homomorphism we're home.
Lean
Formalized as MeasureTheory.addEquivAddHaarChar_prodCongr.
Sources
LemmaMeasureTheory.addEquivAddHaarChar_piCongrRight#
If \(A_i\) are a finite collection of locally compact topological abelian groups, with \(\phi_i:A_i\to A_i\) additive homeomorphisms, then \(d_{\prod_i A_i}(\prod_i\phi_i)=\prod_i d_{A_i}(\phi_i)\).
Proof
Induction on the size of the finite set, using the previous lemma.
Lean
Formalized as MeasureTheory.addEquivAddHaarChar_piCongrRight.
Sources
Uses 1 · Used by 1
LemmaMeasureTheory.ringHaarChar_prod#
If \(R\) and \(S\) are locally compact topological rings, then \(\delta_{R\times S}(r,s)=\delta_R(r)\times\delta_S(s)\).
Proof
Follows immediately from lemma MeasureTheory.addEquivAddHaarChar_prodCongr.
Lean
Formalized as MeasureTheory.ringHaarChar_prod.
Sources
Uses 1
LemmaMeasureTheory.ringHaarChar_pi#
If \(R_i\) are a finite collection of locally compact topological rings, and \(u_i\in R_i^\times\) then \(\delta_{\prod_i R_i}((u_i)_i)=\prod_i\delta_{R_i}(u_i)\).
Proof
Follows immediately from lemma MeasureTheory.addEquivAddHaarChar_piCongrRight.
Lean
Formalized as MeasureTheory.ringHaarChar_pi.
Sources
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.