MetaplecticPrimalFinite.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Compact support turns the literal completed sum, at every translated height, into the finite primary cube polynomial used by Montgomery--Vaughan.

def OAI.CubicFirstMoment.metaplecticPrimaryPair line 14
lemma OAI.CubicFirstMoment.metaplecticPrimaryPair_injective line 17
def OAI.CubicFirstMoment.metaplecticPrimalSupport line 21
def OAI.CubicFirstMoment.metaplecticPrimalElementSupport line 25
lemma OAI.CubicFirstMoment.metaplecticPrimalSupport_of_nonzero line 28
def OAI.CubicFirstMoment.metaplecticHeightCompleted line 56
lemma OAI.CubicFirstMoment.metaplecticHeightCompleted_zero line 62
theorem OAI.CubicFirstMoment.metaplecticHeightCompleted_finite line 70
Source documentation
Exact finite support, independent of the height parameter.
```
theorem metaplecticHeightCompleted_finite (r : Eisenstein) (ℓ : ℤ) (W : ℝ → ℂ)
    {X B V : ℝ} (hX : 0 < X) (hBV : B*X ≤ V)
    (hW : ∀ x : ℝ, B < x → W x = 0) (t : ℝ) :
    metaplecticHeightCompleted r ℓ W X t =
      ∑ du ∈ metaplecticPrimalElementSupport V,
        metaplecticPrimalCoefficient r ℓ W X du*mellinPhase t (norm (metaplecticCubeProduct du)) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.metaplecticHeightCompleted, OAI.CubicFirstMoment.metaplecticPrimalElementSupport, OAI.CubicFirstMoment.metaplecticPrimalCoefficient, OAI.CubicFirstMoment.mellinPhase, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.metaplecticCubeProduct
theorem OAI.CubicFirstMoment.metaplecticHeightCompleted_twist line 86
Source documentation
Exact norm twist needed to apply the published Voronoi formula at height t; its outside scalar has modulus one.
```
theorem metaplecticHeightCompleted_twist (r : Eisenstein) (ℓ : ℤ) (W : ℝ → ℂ)
    {X : ℝ} (hX : 0 < X) (t : ℝ) :
    metaplecticHeightCompleted r ℓ W X t = mellinPhase t X*
      metaplecticCompleted r ℓ (fun x => W x*mellinPhase t x) X := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.metaplecticHeightCompleted, OAI.CubicFirstMoment.mellinPhase, OAI.CubicFirstMoment.metaplecticCompleted
lemma OAI.CubicFirstMoment.metaplecticPrimalElementSupport_primary line 112
lemma OAI.CubicFirstMoment.metaplecticPrimalElementSupport_size line 118

theorem OAI.CubicFirstMoment.metaplecticHeightCompleted_meanAbsolute_sq line 126

Source documentation

The mean estimate now applies to the original infinite completed series, with finiteness and all coefficient bounds discharged.

theorem metaplecticHeightCompleted_meanAbsolute_sq {ε C : ℝ} (hε : 0 < ε)
    (hMV : MontgomeryVaughanBound C) (hC : 0 ≤ C) :
    ∃ K : ℝ, 0 < K ∧ ∀ r : Eisenstein, primary r →
      ∀ (ℓ : ℤ) (W : ℝ → ℂ) (X B V M T u : ℝ), 0 < X → B*X ≤ V →
      (∀ x : ℝ, B < x → W x = 0) → (∀ x : ℝ, ‖W x‖ ≤ M) →
      1 ≤ V → 0 ≤ M → 0 < T →
      ((∫ t in T..2*T, ‖metaplecticHeightCompleted r ℓ W X (t+u)‖)/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.metaplecticHeightCompleted