MetaplecticFreeMean.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The free primary variable in each retained metaplectic support block has inverse-square-root coefficients. Its actual energy and rational norm multiplicity give the ordinary mean-value bound.

lemma OAI.CubicFirstMoment.metaplectic_free_dyad_energy line 15

theorem OAI.CubicFirstMoment.metaplectic_free_meanAbsolute_sq line 37

Source documentation

The actual free-primary dyad mean; the only analytic input is MV.

theorem metaplectic_free_meanAbsolute_sq {ε C : ℝ} (hε : 0 < ε)
    (hMV : MontgomeryVaughanBound C) (hC : 0 ≤ C) :
    ∃ D : ℝ, 0 < D ∧ ∀ (S : Finset Eisenstein), (∀ b ∈ S, primary b) →
      ∀ (v : Eisenstein → ℂ) (L K T u : ℝ) (ℓ : ℤ),
      1 ≤ L → 0 < T → (∀ b ∈ S, L/2 ≤ norm b ∧ norm b ≤ L) →
      (∀ b ∈ S, ‖v b‖^2 ≤ K^2/norm b) →
      ((∫ t in T..2*T, ‖∑ b ∈ S, v b*theta ℓ b*mellinPhase (t+u) (norm b)‖)/T)^2 ≤
        C*D*(1+2*L/T)*L^ε*K^2 := by
…

Mentions: OAI.CubicFirstMoment.MontgomeryVaughanBound, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.theta, OAI.CubicFirstMoment.mellinPhase