OAI/NumberTheory/CubicMoment/Estimates/HeckeDualMoment.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CubicFirstMoment.gammaQuotient_half_strip line 15
2. def OAI.CubicFirstMoment.normalizedDualPolynomial line 27
3. lemma OAI.CubicFirstMoment.finiteHeckeDual_integrand_normalized line 31
4. lemma OAI.CubicFirstMoment.integrable_normalized_dual_kernel line 45
5. lemma OAI.CubicFirstMoment.norm_normalization_sq line 67
6. theorem OAI.CubicFirstMoment.retained_dual_moment_transfer line 81

   Source documentation

   Any common bound on the normalized dual polynomial square-sum gives exactly the factor Z/J in the retained integral square-sum. The constant is independent of the characters, conductors, root numbers and height.

   theorem retained_dual_moment_transfer {ν : Type*}
       (W : ℝ → ℂ) (hW : HasCompactSupport W) (hpos : tsupport W ⊆ Ioi 0)
       (hsm : ContDiff ℝ ∞ W) :
       ∃ C : ℝ, 0 ≤ C ∧ ∀ {ι : Type*} [Fintype ι], ∀ (S : Finset ν) (χ : ι → ν → ℂ) (N : ν → ℝ),
         (∀ v ∈ S, 1 ≤ N v) → ∀ (ε : ι → ℂ) (A : ι → ℝ),
         (∀ i, ‖ε i‖ = 1) → (∀ i, 0 < A i) → ∀ (Z J t B : ℝ),
         1 ≤ Z → 0 < J → 0 ≤ B →
         (∀ τ : ℝ, (∑ i, ‖normalizedDualPolynomial S (χ i) N J (τ-t)‖^2) ≤ B) →
         (∑ i, ‖((1/(2*Real.pi):ℝ):ℂ)*∫ τ : ℝ,
           mellin W ((1/2:ℂ)+(τ:ℂ)*Complex.I)*(Z:ℂ)^((1/2:ℂ)+(τ:ℂ)*Complex.I)*
             finiteHeckeDual S (χ i) N (ε i) (A i)
               ((1/2:ℂ)+((τ-t:ℝ):ℂ)*Complex.I)‖^2) ≤ C*(Z/J)*B := by
   …

   Mentions: OAI.CubicFirstMoment.normalizedDualPolynomial, OAI.CubicFirstMoment.finiteHeckeDual