MetaplecticBlockMean.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Mean value of an actual retained free-variable block, with all coefficient amplitudes supplied by the literal Voronoi coefficient bound.

lemma OAI.CubicFirstMoment.metaplectic_block_frequency line 13

theorem OAI.CubicFirstMoment.metaplectic_actual_block_mean line 25

Source documentation

The finite subset can include arbitrary further restrictions. In particular this applies to each actual norm dyad of the retained sum.

theorem metaplectic_actual_block_mean {ε M : ℝ} (hε : 0 < ε)
    (hMV : MontgomeryVaughanBound M) (hM : 0 ≤ M) :
    ∃ D : ℝ, 0 < D ∧ ∀ (a : Eisenstein → MetaplecticDualArgument → ℂ)
      (C : ℝ), 0 ≤ C → ∀ r : Eisenstein, primary r →
      ∀ (d : PrimaryArgument) (ℓ j : ℤ), -1 ≤ j → ∀ (ζ : Eisensteinˣ)
      (h h' : Eisenstein), primary h → primary h' →
      ∀ (S : Finset Eisenstein) (n : Eisenstein → MetaplecticDualArgument),
      (∀ w ∈ S, primary w) → (∀ w ∈ S, IsCoprime w r) →
      (∀ w ∈ S, metaplecticFrequency (n w) =
        traceLambda^j*(ζ.val:ℂ)*(h:ℂ)*(w:ℂ)*(h':ℂ)^3) →
      (∀ w ∈ S, ‖a r (n w)‖ ≤ C*3^((max j 0:ℤ)/3:ℝ)*Real.sqrt (norm h')) →
      ∀ L T u : ℝ, 1 ≤ L → 0 < T →
…

Mentions: OAI.CubicFirstMoment.MontgomeryVaughanBound, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.MetaplecticDualArgument, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.PrimaryArgument, OAI.CubicFirstMoment.metaplecticFrequency, OAI.CubicFirstMoment.traceLambda, OAI.CubicFirstMoment.norm