MetaplecticPrimalShort.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The short-polynomial branch of the completed angular height bound.

lemma OAI.CubicFirstMoment.metaplectic_short_height_factor line 10

theorem OAI.CubicFirstMoment.metaplecticHeightCompleted_short_mean line 27

Source documentation

For V≤sqrt(R)T² the literal completed angular sum has mean size O(V^(1/2+epsilon) R^(1/4) sqrt(T)); the displayed square root keeps the exact coefficient constants and avoids hidden normalization factors.

theorem metaplecticHeightCompleted_short_mean {ε C : ℝ} (hε : 0 < ε)
    (hMV : MontgomeryVaughanBound C) (hC : 0 ≤ C) :
    ∃ K : ℝ, 0 < K ∧ ∀ r : Eisenstein, primary r →
      ∀ (ℓ : ℤ) (W : ℝ → ℂ) (X B V M T u R : ℝ),
      0 < X → B*X ≤ V → (∀ x : ℝ, B < x → W x = 0) →
      (∀ x : ℝ, ‖W x‖ ≤ M) → 1 ≤ V → 0 ≤ M → 1 ≤ T → 1 ≤ R →
      V ≤ Real.sqrt R*T^2 →
      (∫ t in T..2*T, ‖metaplecticHeightCompleted r ℓ W X (t+u)‖)/T ≤
        Real.sqrt (3*C*K*V^(1+ε)*Real.sqrt R*T)*M := by
…

Mentions: OAI.CubicFirstMoment.MontgomeryVaughanBound, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.metaplecticHeightCompleted