AngularDualMoment.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The shifted Gamma factor has unit modulus on the symmetry line. Thus the actual angular retained integral obeys the same finite moment transfer, with no angular loss in the sieve or conductor parameter.

lemma OAI.CubicFirstMoment.angularGammaQuotient_half_strip line 14
lemma OAI.CubicFirstMoment.angular_finite_dual_symmetry_integrand line 27
lemma OAI.CubicFirstMoment.angularFiniteHeckeDual_integrand_normalized line 50
lemma OAI.CubicFirstMoment.integrable_angular_normalized_dual_kernel line 64

theorem OAI.CubicFirstMoment.angular_retained_dual_moment_transfer line 89

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 angular_retained_dual_moment_transfer {ν : Type*}
    (k : ℝ) (hk : 0 ≤ k)
    (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)*
          angularFiniteHeckeDual S (χ i) N (ε i) (A i) k
…

Mentions: OAI.CubicFirstMoment.normalizedDualPolynomial, OAI.CubicFirstMoment.angularFiniteHeckeDual