Definitions/Def_AutomorphicForm_GL2TwistedMonomialFibres.lean

Fix g \in \mathrm{GL}_2(\mathbb{C}) and write \bar g for its entrywise conjugate (the conjEntries of the ambient module) and g^{*} for its conjugate transpose. Four scalar invariants are introduced: invFrobSq T = \operatorname{Re}\operatorname{tr}(g g^{*}), the sum of the squared moduli of the entries; invTraceNorm y = \operatorname{tr}(g\bar g) \in \mathbb{C}; invSecondRe = \operatorname{Re}\operatorname{tr}\bigl((g\bar g)(g g^{*})\bigr); and invAbsDet d = |\det g|. From these, invDifference is E = \bigl(\operatorname{Re}\operatorname{tr}((g\bar g)(gg^{*})) - T\,\operatorname{Re} y + 2d^{2}\bigr)/d, and monomialInput of bidegree (i,l) is the real number \Bigl(\tfrac{T - \operatorname{Re} y + E}{2(T+2d)}\Bigr)^{i}\Bigl(\tfrac{T - \operatorname{Re} y - E}{2(T-2d)}\Bigr)^{l}. Divisions follow the Lean convention that division by zero is zero, so on the locus T = 2d the second base is read as 0.

The remaining definitions are the shapes in which these monomials are expected to transform. fibreMonomialFactor is (T-x)^{i+l}/\bigl((T+2d)^{i}(T-2d)^{l}\bigr) for real parameters T, d, x; fibreArcIntegral is \int_{-\Psi/2}^{\Psi/2}\cos^{2i}\psi\,\sin^{2l}\psi\,d\psi; and ellipticArcLength is \arccos\bigl((2r - T\cos\theta)/(T - 2r\cos\theta)\bigr). Then ellipticFibreTerm is the complex number obtained from the real quantity (4\pi\sin\theta/r)\cdot (the monomial factor at d = r, x = 2r\cos\theta) \cdot (the arc integral over an arc of length ellipticArcLength), while splitFibreTerm at (a_1,a_2) is one half of the monomial factor at d = \sqrt{a_1 a_2}, x = a_1 + a_2, times the arc integral over \Psi = 2\pi, i.e. the full circle. Finally, for a complex-valued profile c on the levels T, ellipticFibreSide is \int_{T > 2r} c(T)\,\cdot ellipticFibreTerm and splitFibreSide is \int_{T > a_1+a_2} c(T)\,\cdot splitFibreTerm, both Lebesgue integrals over the indicated half-lines.