Definitions/Def_LanglandsTunnell_CubicInduction_AdelicEpstein.lean

Throughout, \mathbb{A} denotes the adele ring of \mathbb{Q} (as the adele ring of \mathcal{O}_{\mathbb{Q}} over \mathbb{Q}), and \widehat{\mathbb{Z}}^{\times} denotes IsDedekindDomain.FiniteAdeleRing.unitIdeles, the subgroup of those units of the finite adele ring whose value at every height-one prime, and whose inverse's value at every height-one prime, lies in the corresponding ring of integers. A real number t is transported into the completion of \mathbb{Q} at its (real) infinite place by ofReal, the inverse of the ring isomorphism of that completion with \mathbb{R}. From this, archIdele t is the idele which is 1 for t=0 and otherwise the image of the unit t under TateGlobal.archUnitHom at the infinite place, i.e. the idele with archimedean component t and component 1 elsewhere; dually finUnitIdele u sends u\in\widehat{\mathbb{Z}}^{\times} to the idele with finite part u and archimedean part 1, via AdelicLevel.finIncl. A rational row vector \xi\in\mathbb{Q}^{3} is read coordinatewise in \mathbb{A}^{3} by adelicDiag, and point t u g ξ, for g\in \mathrm{GL}_3(\mathbb{A}), is the row vector \xi g with every coordinate multiplied by the adele underlying \mathrm{archIdele}(t)\cdot\mathrm{finUnitIdele}(u).

scaleMeasure is Lebesgue measure on \mathbb{R} restricted to (0,\infty) with density t^{-1}, that is dt/t. For \Phi:\mathbb{A}^{3}\to\mathbb{C}, latticeSum Φ t u g is the unconditional sum of \Phi(\mathrm{point}\ t\,u\,g\,\xi) over the subtype of non-zero \xi\in\mathbb{Q}^{3} (hence 0 when the family fails to be summable). Given a \sigma-algebra on \widehat{\mathbb{Z}}^{\times} and a measure du on it, epstein is \|\det g\|^{\sigma}, where \|\cdot\| is TateGlobal.ideleNorm (the idele norm defined through the Haar scaling character), times the Bochner integral over scaleMeasure of t^{3\sigma} times the Bochner integral of the lattice sum against du; non-integrable integrands contribute 0. epsteinPlus is the [0,\infty]-valued analogue, formed with \|\Phi\| and with the sum over non-zero \xi and both integrals taken as lower integrals in [0,\infty]. Finally unitIdeleMeasurableSpace is the \sigma-algebra on \widehat{\mathbb{Z}}^{\times} pulled back along u\mapsto \mathrm{finUnitIdele}(u) from the Borel \sigma-algebra NumberField.AdelicHaar.adeleBorel on \mathbb{A}, for which measurable_finUnitIdele records that this pullback map is measurable.