HeckeSymmetry.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The scalar factors on the symmetry line in the primitive Hecke functional equation. These identities apply also to fixed infinity type. They keep conductor-dependent phases outside the dual polynomial.

def OAI.CubicFirstMoment.heckeGammaRatio line 14
lemma OAI.CubicFirstMoment.norm_heckeGammaRatio line 18
def OAI.CubicFirstMoment.heckeSymmetryFactor line 33
Source documentation
D includes the fixed field factor in the completed L-function.
```
def heckeSymmetryFactor (ε : ℂ) (D Z k t τ : ℝ) : ℂ :=
…
```
lemma OAI.CubicFirstMoment.norm_heckeSymmetryFactor line 36

lemma OAI.CubicFirstMoment.heckeSymmetry_square_sum line 43

Source documentation

The entire character-dependent multiplier can be removed from the square-sum norm before applying a common integral majorant.

lemma heckeSymmetry_square_sum {ι : Type*} (S : Finset ι)
    (ε : ι → ℂ) (D : ι → ℝ) (Z k t τ : ℝ) (v : ι → ℂ)
    (hε : ∀ i ∈ S, ‖ε i‖ = 1) (hk : 0 ≤ k) :
    (∑ i ∈ S, ‖heckeSymmetryFactor (ε i) (D i) Z k t τ * v i‖^2) =
      ∑ i ∈ S, ‖v i‖^2 := by
…

Mentions: OAI.CubicFirstMoment.heckeSymmetryFactor