MetaplecticPrefixMass.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The first retained-block majorant is summable with arbitrary small powers of its finite norm cutoff and its squarefree level.

lemma OAI.CubicFirstMoment.metaplectic_divisor_card_power line 12
theorem OAI.CubicFirstMoment.metaplectic_first_prefix_mass line 21

theorem OAI.CubicFirstMoment.metaplectic_second_prefix_mass line 78

Source documentation

The second scalar weight is smaller than the first one termwise; the same arbitrary small-power estimate therefore suffices for the application.

theorem metaplectic_second_prefix_mass {ε ρ : ℝ} (hε : 0 < ε)
    (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) :
    ∃ C : ℝ, 0 < C ∧ ∀ r : Eisenstein, primary r →
      ∀ (P : Finset (MetaplecticDyadPrefix r)) (J : ℝ), 0 < J →
      (∀ p ∈ P, ∃ k : ℕ, p.2.2.2.2.val ∣ r^k) →
      (∀ p ∈ P, norm p.1 ≤ J ∧ norm p.2.2.2.2 ≤ J) →
      (∑ p ∈ P, norm p.1^(-(5/2):ℝ)*ρ^p.2.1*norm p.2.2.2.2^(-(3/2):ℝ)) ≤
        C*J^ε*norm r^(2*ε) := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.MetaplecticDyadPrefix, OAI.CubicFirstMoment.norm