HeckeMajorant.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A common scalar majorant permits integration before the finite character square-sum. The conductor and root number remain row scalars.

theorem OAI.CubicFirstMoment.common_majorant_square_sum line 15

theorem OAI.CubicFirstMoment.hecke_common_majorant_square_sum line 46

Source documentation

A simultaneous character average can use one norm-shift measure: the conductor-dependent Hecke factor contributes exactly no loss.

theorem hecke_common_majorant_square_sum {ι : Type*} [Fintype ι]
    (ε : ι → ℂ) (D : ι → ℝ) (Z k t : ℝ) (P W : ι → ℝ → ℂ)
    (w : ℝ → ℝ) {B : ℝ} (hB : 0 ≤ B)
    (hε : ∀ i, ‖ε i‖ = 1) (hk : 0 ≤ k)
    (hInt : ∀ i, Integrable (fun τ =>
      W i τ * heckeSymmetryFactor (ε i) (D i) Z k t τ * P i τ))
    (hw : Integrable w) (hw0 : ∀ τ, 0 ≤ w τ)
    (hW : ∀ i τ, ‖W i τ‖ ≤ w τ)
    (hP : ∀ τ, (∑ i, ‖P i τ‖^2) ≤ B) :
    (∑ i, ‖∫ τ : ℝ,
      W i τ * heckeSymmetryFactor (ε i) (D i) Z k t τ * P i τ‖^2) ≤
        (∫ τ : ℝ, w τ)^2*B := by
…

Mentions: OAI.CubicFirstMoment.heckeSymmetryFactor