MetaplecticShortScale.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The short completed mean with an arbitrary fixed upper support endpoint; the arithmetic length X is kept separate from that endpoint.

lemma OAI.CubicFirstMoment.metaplectic_short_support_factor line 11

theorem OAI.CubicFirstMoment.metaplecticHeightCompleted_short_scaled_mean line 28

Source documentation

Actual finite primal coefficients supply this estimate, including an arbitrary fixed support endpoint.

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

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