MetaplecticCubeMean.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Montgomery--Vaughan applied to the actual finite cube-completed angular Gauss sum. Both the rational norm multiplicity and the original coefficient energy are supplied by proved arithmetic lemmas.

lemma OAI.CubicFirstMoment.metaplectic_cube_polynomial_collect line 14
lemma OAI.CubicFirstMoment.metaplectic_cube_output_primary line 28
lemma OAI.CubicFirstMoment.metaplectic_cube_norm_frequencies line 37

theorem OAI.CubicFirstMoment.metaplectic_primal_meanAbsolute_sq line 57

Source documentation

The one-sided height mean for the literal completed angular coefficients. The only analytic hypothesis is the published ordinary Montgomery--Vaughan theorem.

theorem metaplectic_primal_meanAbsolute_sq {ε C : ℝ} (hε : 0 < ε)
    (hMV : MontgomeryVaughanBound C) (hC : 0 ≤ C) :
    ∃ K : ℝ, 0 < K ∧ ∀ (S : Finset (Eisenstein × Eisenstein)),
      (∀ du ∈ S, primary du.1 ∧ primary du.2) →
      ∀ (r : Eisenstein), primary r → ∀ (ℓ : ℤ) (W : ℝ → ℂ) (X V M T u : ℝ),
      1 ≤ V → 0 ≤ M → 0 < T →
      (∀ du ∈ S, norm (metaplecticCubeProduct du) ≤ V) →
      (∀ du ∈ S, ‖W (norm (metaplecticCubeProduct du)/X)‖ ≤ M) →
      ((∫ t in T..2*T, ‖∑ du ∈ S, metaplecticPrimalCoefficient r ℓ W X du*
        mellinPhase (t+u) (norm (metaplecticCubeProduct du))‖)/T)^2 ≤
          C*K*(1+2*V/T)*V^(1+ε)*M^2 := by
…

Mentions: OAI.CubicFirstMoment.MontgomeryVaughanBound, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.metaplecticCubeProduct, OAI.CubicFirstMoment.metaplecticPrimalCoefficient, OAI.CubicFirstMoment.mellinPhase