MetaplecticSupportedSum.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Supported primary factors in the retained metaplectic sum have convergent weighted Euler products with arbitrarily small level loss.

lemma OAI.CubicFirstMoment.idealExponent_support_of_dvd_power line 14

theorem OAI.CubicFirstMoment.primary_supported_norm_sum line 29

Source documentation

The exponent δ of the convergent supported sum is fixed independently of the arbitrarily small loss ε in the level.

theorem primary_supported_norm_sum {ε δ : ℝ} (hε : 0 < ε) (hδ : 0 < δ) :
    ∃ C : ℝ, 0 < C ∧ ∀ r : Eisenstein, primary r →
      ∀ (S : Finset Eisenstein) (J : ℝ), (∀ b ∈ S, primary b) →
      (∀ b ∈ S, ∃ k : ℕ, b ∣ r^k) → (∀ b ∈ S, norm b ≤ J) →
      (∑ b ∈ S, norm b^(-δ)) ≤ C*norm r^ε := by
…

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