HeckeFunctionalEquation.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Algebra of the published primitive Hecke functional equation. The completion uses A = sqrt(3 D)/(2 pi), where D is the ideal conductor norm. See Watkins (2011), Section 3.6, and Rajan (1998), Section 1, pp. 281--283 for the fixed infinity-type completion. The uncompleted and symmetry-line identities follow from that exact equation.

def OAI.CubicFirstMoment.heckeCompleted line 13
def OAI.CubicFirstMoment.HeckeFunctionalEquation line 21
Source documentation
The precisely normalized functional-equation input, supplied for an actual primitive character and its contragredient, away from the gamma poles. The regular-point restriction is necessary because mathlib totalizes Gamma at its poles; the analytic completion has removable singularities there, whereas the pointwise product need not agree.
```
def HeckeFunctionalEquation (A k : ℝ) (ε : ℂ) (L Ldual : ℂ → ℂ) : Prop :=
…
```
theorem OAI.CubicFirstMoment.hecke_uncompleted line 26
lemma OAI.CubicFirstMoment.hecke_conductor_phase line 47
theorem OAI.CubicFirstMoment.hecke_symmetry_line line 58
lemma OAI.CubicFirstMoment.hecke_scale_phase line 88

theorem OAI.CubicFirstMoment.hecke_symmetry_integrand line 102

Source documentation

The exact symmetry-line amplitude and scalar phase. This identity keeps all conductor dependence outside the dual polynomial.

theorem hecke_symmetry_integrand {A Z k : ℝ} (hA : 0 < A) (hZ : 0 < Z)
    (hk : 0 ≤ k) {ε : ℂ} {L Ldual : ℂ → ℂ}
    (hFE : HeckeFunctionalEquation A k ε L Ldual) (W : ℂ → ℂ) (t τ : ℝ) :
    W ((1/2:ℂ)+(τ:ℂ)*Complex.I) * (Z:ℂ)^((1/2:ℂ)+(τ:ℂ)*Complex.I) *
      L ((1/2:ℂ)+((τ-t:ℝ):ℂ)*Complex.I) =
    (Real.sqrt Z:ℂ) * W ((1/2:ℂ)+(τ:ℂ)*Complex.I) *
      heckeSymmetryFactor ε (A^2) Z k t τ *
        Ldual ((1/2:ℂ)-((τ-t:ℝ):ℂ)*Complex.I) := by
…

Mentions: OAI.CubicFirstMoment.HeckeFunctionalEquation, OAI.CubicFirstMoment.heckeSymmetryFactor

lemma OAI.CubicFirstMoment.norm_hecke_symmetry_line line 114